Cleaning of the trailing spaces

LICENSE

@@ -146,7 +146,7 @@ such a program is covered only if its contents constitute a work based
 on the Library (independent of the use of the Library in a tool for
 writing it).  Whether that is true depends on what the Library does
 and what the program that uses the Library does.
-  
+
   1. You may copy and distribute verbatim copies of the Library's
 complete source code as you receive it, in any medium, provided that
 you conspicuously and appropriately publish on each copy an

Makefile

@@ -25,7 +25,6 @@ run: all
 	@echo "It is accessible at: http://localhost:8000"
 	@cd www && python -m SimpleHTTPServer 8000
 
-
 check-deps: \
 	which-opam which-lua5.1 pkg-lua-filesystem opam-config which-markdown
 

POLICY.md

@@ -27,15 +27,15 @@ tool.
 
 The repository contains package for development versions of Coq.  Typically
 .dev packages for Coq branches.  The repository is self contained.  The
-repository is intended to be used by developers only. 
+repository is intended to be used by developers only.
 
 ### extra-dev
 
 The repository contains packages for development versions of external
 contributions to Coq.  Typically .dev packages following the branches of the
 extension.  The repository is not self contained, i.e. a package may depend on
 a development version of Coq part of the `core-dev` repository.  The repository
-is intended to be used by developers only. 
+is intended to be used by developers only.
 
 ## 2. Policy for stable-$VERSION
 
@@ -48,7 +48,7 @@ The repository shall contain software that works with Coq $VERSION and that
 won't break for the whole lifetime of Coq $VERSION.  Coq extensions packages
 are maintained by their corresponding authors or by the Coq team.  Updates are
 accepted only if they don't break anything (like for Coq patch level releases)
-or if a transition strategy is provided (more on that in section 2.3).  
+or if a transition strategy is provided (more on that in section 2.3).
 The repository is intended to be used by users preferring stability to bleeding
 edge and users not familiar with the OPAM tool.
 

README.md

@@ -51,7 +51,7 @@ In particular we use the `tags` field of the `opam` file as follows:
  2. strings beginning with `category:` are considered as `categories`
  3. a string beginning with `date:` is the date the software was last updated
     (not the package)
- 
+
 Example:
 
     tags: [ "keyword:cool" "keyword:stuff" "category:Some/Category" "date:1/1/1970" ]

core-dev/LICENSE

@@ -19,4 +19,3 @@ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
-

core-dev/packages/coq.8.3.dev/descr

@@ -1 +1 @@
-Formal proof management system.
+Formal proof management system.

core-dev/packages/coq.8.3.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "http://coq.inria.fr/"
 bug-reports: "https://coq.inria.fr/bugs/"
@@ -10,4 +10,4 @@ build: [
 ]
 depends: [
   "camlp5"
-]
+]

core-dev/packages/coq.8.4.dev+ltacprof/descr

@@ -1 +1 @@
-Formal proof management system.
+Formal proof management system.

core-dev/packages/coq.8.4.dev+ltacprof/files/ltac-profiling-0.2-rebuilt.patch

@@ -5,11 +5,11 @@ index f13a3d1..9e83d0a 100644
 @@ -109,6 +109,39 @@ let utf8_length s =
    done ;
    !cnt
- 
+
 +(* Variant of String.sub for UTF8 character positions *)
 +let utf8_sub s start_u len_u =
 +  let len_b = String.length s
-+  and end_u = start_u + len_u   
++  and end_u = start_u + len_u
 +  and cnt = ref 0
 +  and nc = ref 0
 +  and p = ref 0 in
@@ -48,7 +48,7 @@ index 695bcbc..4d8c61d 100644
 +++ b/lib/pp.mli
 @@ -122,3 +122,6 @@ val msg_warn : string -> unit
  val msg_debug : std_ppcmds -> unit
- 
+
  val string_of_ppcmds : std_ppcmds -> string
 +
 +val utf8_length : string -> int
@@ -88,14 +88,14 @@ index 0000000..9e5797b
 +  if add_total then e.total <- e.total +. total;
 +  e.local <- e.local +. local;
 +  e.ncalls <- e.ncalls + ncalls;
-+  if add_total then e.max_total <- max e.max_total max_total				       
++  if add_total then e.max_total <- max e.max_total max_total
 +
 +type treenode = {entry : entry; children : (string, treenode) Hashtbl.t}
 +let stack = ref [{entry=empty_entry(); children=Hashtbl.create 20}]
 +
 +let on_stack = Hashtbl.create 5
 +
-+let get_node c table = 
++let get_node c table =
 +  try Hashtbl.find table c
 +  with Not_found ->
 +    let new_node = {entry=empty_entry(); children=Hashtbl.create 5} in
@@ -108,7 +108,7 @@ index 0000000..9e5797b
 +    (fun s node' -> add_node (get_node s node.children) node')
 +    node'.children
 +
-+let time() = 
++let time() =
 +  let times = Unix.times() in
 +  times.Unix.tms_utime +. times.Unix.tms_stime
 +
@@ -136,21 +136,21 @@ index 0000000..9e5797b
 +       | Proof_type.LtacAtomCall (te,otac) ->
 +	 (Pptactic.pr_glob_tactic (Global.env())
 +	    (Tacexpr.TacAtom (dummy_loc,te)))
-+       | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> 
++       | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
 +	 pr_glob_constr_env (Global.env()) c
 +    ) in
 +  for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
 +  let s = try String.sub s 0 (Util.string_index_from s 0 "(*") with Not_found -> s in
 +  Util.strip s
-+	    
++
 +let do_profile s call_trace f =
 +  if !is_profiling && is_new_call() then
 +    match call_trace with
 +      | (_, _, c) :: _ ->
 +	let s = string_of_call c in
 +	let parent = List.hd !stack in
 +	let node, add_total = try Hashtbl.find on_stack s, false
-+			      with Not_found -> 
++			      with Not_found ->
 +				   let node = get_node s parent.children in
 +				   Hashtbl.add on_stack s node;
 +				   node, true
@@ -169,17 +169,17 @@ index 0000000..9e5797b
 +let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
 +let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
 +let padr n s = str s ++ ws (max 0 (n - utf8_length s))
-+let padr_with c n s = 
++let padr_with c n s =
 +  let ulength = utf8_length s in
 +  let length = String.length s in
-+  str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c)  
++  str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c)
 +
 +let rec list_iter_is_last f = function
 +  | []      -> ()
 +  | [x]     -> f true x
 +  | x :: xs -> f false x; list_iter_is_last f xs
 +
-+let header() = 
++let header() =
 +  msgnl(str" tactic                                    self  total   calls       max");
 +  msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘")
 +
@@ -197,11 +197,11 @@ index 0000000..9e5797b
 +  print_table all_total indent false n.children
 +
 +and print_table all_total indent first_level table =
-+  let ls = Hashtbl.fold 
-+	     (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l) 
++  let ls = Hashtbl.fold
++	     (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l)
 +      table [] in
 +  match ls with
-+  | [(s,n)]  when (not first_level) ->    
++  | [(s,n)]  when (not first_level) ->
 +     print_node all_total indent (indent^"└") (s,n)
 +  | _ ->
 +     let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in
@@ -219,7 +219,7 @@ index 0000000..9e5797b
 +  let all_total = -. (List.hd !stack).entry.local in
 +  let global = Hashtbl.create 20 in
 +  let rec cumulate table =
-+    Hashtbl.iter 
++    Hashtbl.iter
 +      (fun s node ->
 +	let node' = get_node s global in
 +	add_entry node'.entry true node.entry;
@@ -270,7 +270,7 @@ index 0000000..9e5797b
 +  msgnl(str"");
 +  header();
 +  print_table tactic_total "" true table_tactic
-+	      
++
 +let reset_profile() = stack := [{entry=empty_entry(); children=Hashtbl.create 20}]
 diff --git a/tactics/profile_ltac.mli b/tactics/profile_ltac.mli
 new file mode 100644
@@ -287,7 +287,7 @@ index 0000000..0455e51
 +val print_results : unit -> unit
 +
 +val print_results_tactic : string -> unit
-+			      
++
 +val reset_profile : unit -> unit
 diff --git a/tactics/profile_ltac_tactics.ml b/tactics/profile_ltac_tactics.ml
 new file mode 100644
@@ -303,15 +303,15 @@ index 0000000..d536f40
 +
 +open Profile_ltac
 +
-+let tclSET_PROFILING b = fun gl -> 
-+   set_profiling b; Tacticals.tclIDTAC gl    
++let tclSET_PROFILING b = fun gl ->
++   set_profiling b; Tacticals.tclIDTAC gl
 +
 +TACTIC EXTEND start_profiling
-+  | [ "start" "profiling" ] -> [ tclSET_PROFILING true  ]    
++  | [ "start" "profiling" ] -> [ tclSET_PROFILING true  ]
 +END
-+    
-+TACTIC EXTEND stop_profiling 
-+  | [ "stop" "profiling" ] ->  [ tclSET_PROFILING false ]    
++
++TACTIC EXTEND stop_profiling
++  | [ "stop" "profiling" ] ->  [ tclSET_PROFILING false ]
 +END;;
 +
 +
@@ -341,12 +341,12 @@ index 9572277..f189dab 100644
 --- a/tactics/tacinterp.ml
 +++ b/tactics/tacinterp.ml
 @@ -277,7 +277,7 @@ let lookup_genarg_subst  id = let (_,_,f) = lookup_genarg id in f
- 
+
  let push_trace (loc,ck) = function
    | (n,loc',ck')::trl when ck=ck' -> (n+1,loc,ck)::trl
 -  | trl -> (1,loc,ck)::trl
 +  | trl -> Profile_ltac.entered_call(); (1,loc,ck)::trl
- 
+
  let propagate_trace ist loc id = function
    | VFun (_,lfun,it,b) ->
 @@ -1793,7 +1793,9 @@ and eval_tactic ist = function

core-dev/packages/coq.8.4.dev/descr

@@ -1 +1 @@
-Formal proof management system.
+Formal proof management system.

core-dev/packages/coq.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "http://coq.inria.fr/"
 bug-reports: "https://coq.inria.fr/bugs/"

core-dev/packages/coq.8.5.dev/descr

@@ -1 +1 @@
-Formal proof management system.
+Formal proof management system.

core-dev/packages/coq.8.5.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "http://coq.inria.fr/"
 bug-reports: "https://coq.inria.fr/bugs/"

core-dev/packages/coq.8.5~beta1/descr

@@ -1 +1 @@
-Formal proof management system.
+Formal proof management system.

core-dev/packages/coq.8.5~beta1/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "http://coq.inria.fr/"
 bug-reports: "https://coq.inria.fr/bugs/"

core-dev/packages/coq.dev/descr

@@ -1 +1 @@
-Formal proof management system.
+Formal proof management system.

core-dev/packages/coq.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "http://coq.inria.fr/"
 bug-reports: "https://coq.inria.fr/bugs/"

core-dev/packages/coq.hott/opam

@@ -1,6 +1,6 @@
 opam-version: "1.1"
 build: [
-  [ "./configure" 
+  [ "./configure"
     "-configdir" "%{lib}%/coq/config"
     "-mandir" "%{man}%"
     "-docdir" "%{doc}%"

extra-dev/LICENSE

@@ -19,4 +19,3 @@ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 SOFTWARE.
-

extra-dev/packages/coq:abp/coq:abp.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/abp.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:abp/coq:abp.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/abp.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:additions/coq:additions.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/additions.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:additions/coq:additions.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/additions.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:ails/coq:ails.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/ails.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:ails/coq:ails.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/ails.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:algebra/coq:algebra.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/algebra.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:algebra/coq:algebra.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/algebra.git;a=tree"
 license: "LGPL 2"

extra-dev/packages/coq:amm11262/coq:amm11262.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/amm11262.git;a=tree"
 license: "LGPL"

extra-dev/packages/coq:amm11262/coq:amm11262.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/amm11262.git;a=tree"
 license: "LGPL"

extra-dev/packages/coq:angles/coq:angles.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/angles.git;a=tree"
 license: "Proprietary"

extra-dev/packages/coq:angles/coq:angles.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/angles.git;a=tree"
 license: "Proprietary"

extra-dev/packages/coq:area-method/coq:area-method.8.4.dev/descr

@@ -1,6 +1,5 @@
 The Chou, Gao and Zhang area method.
 
-
 This contribution is the implementation of the Chou, Gao and Zhang's area method decision procedure for euclidean plane geometry.
 This development contains a partial formalization of the book "Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems" by Chou, Gao and Zhang.
 The examples shown automatically (there are more than 100 examples) includes the Ceva, Desargues, Menelaus, Pascal, Centroïd, Pappus, Gauss line, Euler line, Napoleon theorems.

extra-dev/packages/coq:area-method/coq:area-method.dev/descr

@@ -1,6 +1,5 @@
 The Chou, Gao and Zhang area method.
 
-
 This contribution is the implementation of the Chou, Gao and Zhang's area method decision procedure for euclidean plane geometry.
 This development contains a partial formalization of the book "Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems" by Chou, Gao and Zhang.
 The examples shown automatically (there are more than 100 examples) includes the Ceva, Desargues, Menelaus, Pascal, Centroïd, Pappus, Gauss line, Euler line, Napoleon theorems.

extra-dev/packages/coq:atbr/coq:atbr.8.4.dev/opam

@@ -1,4 +1,4 @@
-opam-version: "1.1" 
+opam-version: "1.1"
 maintainer: "[email protected]"
 homepage: "https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq-contribs/atbr.git;a=tree"
 license: "LGPL"