From 4e70791036a1ab189579e109b428f46f45698b59 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 12:13:04 +0200
Subject: Adding a fold_glob_constr_with_binders combinator.

Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.

Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
---
 pretyping/glob_ops.ml  | 153 ++++++++++++++++---------------------------------
 pretyping/glob_ops.mli |   1 +
 2 files changed, 51 insertions(+), 103 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ebbfa195f0..aa296aace7 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -214,55 +214,57 @@ let fold_glob_constr f acc = function
     f acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
-let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
+let fold_return_type_with_binders f g v acc (na,tyopt) =
+  Option.fold_left (f (name_fold g na v)) acc tyopt
+
+let fold_glob_constr_with_binders g f v acc = function
+  | GVar _ -> acc
+  | GApp (_,c,args) -> List.fold_left (f v) (f v acc c) args
+  | GLambda (_,na,_,b,c) | GProd (_,na,_,b,c) ->
+    f (name_fold g na v) (f v acc b) c
+  | GLetIn (_,na,b,t,c) ->
+    f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c
+  | GCases (_,_,rtntypopt,tml,pl) ->
+    let fold_pattern acc (_,idl,p,c) = f (List.fold_right g idl v) acc c in
+    let fold_tomatch (v',acc) (tm,(na,onal)) =
+      (Option.fold_left (fun v'' (_,_,nal) -> List.fold_right (name_fold g) nal v'')
+                        (name_fold g na v') onal,
+       f v acc tm) in
+    let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
+    let acc = Option.fold_left (f v') acc rtntypopt in
+    List.fold_left fold_pattern acc pl
+  | GLetTuple (_,nal,rtntyp,b,c) ->
+    f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c
+  | GIf (_,c,rtntyp,b1,b2) ->
+    f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2
+  | GRec (_,_,idl,bll,tyl,bv) ->
+    let f' i acc fid =
+      let v,acc =
+	List.fold_left
+	  (fun (v,acc) (na,k,bbd,bty) ->
+            (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty))
+          (v,acc)
+          bll.(i) in
+      f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
+    Array.fold_left_i f' acc idl
+  | GCast (_,c,k) ->
+    let acc = match k with
+      | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
+    f v acc c
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
-let same_id na id = match na with
-| Anonymous -> false
-| Name id' -> Id.equal id id'
+let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
 let occur_glob_constr id =
-  let rec occur = function
+  let rec occur barred acc = function
     | GVar (loc,id') -> Id.equal id id'
-    | GApp (loc,f,args) -> (occur f) || (List.exists occur args)
-    | GLambda (loc,na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GProd (loc,na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GLetIn (loc,na,b,t,c) ->
-      (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	(occur_option rtntypopt)
-        || (List.exists (fun (tm,_) -> occur tm) tml)
-	|| (List.exists occur_pattern pl)
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	occur_return_type rtntyp id
-        || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c))
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-        not (Array.for_all4 (fun fid bl ty bd ->
-          let rec occur_fix = function
-              [] -> not (occur ty) && (Id.equal fid id || not(occur bd))
-            | (na,k,bbd,bty)::bl ->
-                not (occur bty) &&
-                (match bbd with
-                    Some bd -> not (occur bd)
-                  | _ -> true) &&
-                (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
-          occur_fix bl)
-          idl bl tyl bv)
-    | GCast (loc,c,k) -> (occur c) || (match k with CastConv t
-      | CastVM t | CastNative t -> occur t | CastCoerce -> false)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
-
-  and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c)
-
-  and occur_option = function None -> false | Some p -> occur p
-
-  and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt
-
-  in occur
-
+    | c ->
+       (* [g] looks if [id] appears in a binding position, in which
+          case, we don't have to look in the corresponding subterm *)
+       let g id' barred = barred || Id.equal id id' in
+       let f barred acc c = acc || not barred && occur false acc c in
+       fold_glob_constr_with_binders g f barred acc c in
+  occur false false
 
 let add_name_to_ids set na =
   match na with
@@ -270,64 +272,9 @@ let add_name_to_ids set na =
     | Name id -> Id.Set.add id set
 
 let free_glob_vars =
-  let rec vars bounded vs = function
-    | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
-    | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
-	let vs' = vars bounded vs ty in
-	let bounded' = add_name_to_ids bounded na in
-       vars bounded' vs' c
-    | GLetIn (loc,na,b,ty,c) ->
-	let vs' = vars bounded vs b in
-	let vs'' = Option.fold_left (vars bounded) vs' ty in
-	let bounded' = add_name_to_ids bounded na in
-       vars bounded' vs'' c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	let vs1 = vars_option bounded vs rtntypopt in
-	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
-	List.fold_left (vars_pattern bounded) vs2 pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	let vs1 = vars_return_type bounded vs rtntyp in
-	let vs2 = vars bounded vs1 b in
-	let bounded' = List.fold_left add_name_to_ids bounded nal in
-	vars bounded' vs2 c
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	let vs1 = vars_return_type bounded vs rtntyp in
-	let vs2 = vars bounded vs1 c in
-	let vs3 = vars bounded vs2 b1 in
-	vars bounded vs3 b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bounded' = Array.fold_right Id.Set.add idl bounded in
-	let vars_fix i vs fid =
-	  let vs1,bounded1 =
-	    List.fold_left
-	      (fun (vs,bounded) (na,k,bbd,bty) ->
-		 let vs' = vars_option bounded vs bbd in
-		 let vs'' = vars bounded vs' bty in
-		 let bounded' = add_name_to_ids bounded na in
-		 (vs'',bounded')
-	      )
-	      (vs,bounded')
-	      bl.(i)
-	  in
-	  let vs2 = vars bounded1 vs1 tyl.(i) in
-	  vars bounded1 vs2 bv.(i)
-	in
-	Array.fold_left_i vars_fix vs idl
-    | GCast (loc,c,k) -> let v = vars bounded vs c in
-	(match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
-  and vars_pattern bounded vs (loc,idl,p,c) =
-    let bounded' = List.fold_right Id.Set.add idl bounded  in
-    vars bounded' vs c
-
-  and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p
-
-  and vars_return_type bounded vs (na,tyopt) =
-    let bounded' = add_name_to_ids bounded na in
-    vars_option bounded' vs tyopt
-  in
+  let rec vars bound vs = function
+    | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs
+    | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in
   fun rt ->
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 55e6b6533f..af2834e498 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -37,6 +37,7 @@ val map_glob_constr_left_to_right :
 val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit
 
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
+val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
-- 
cgit v1.2.3


From b4936da085b19ad508346d8e07ce1e922ef79c2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 15:05:16 +0200
Subject: Using fold_glob_constr_with_binders to code bound_glob_vars.

To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.

This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
---
 pretyping/glob_ops.ml | 57 ++++++++-------------------------------------------
 1 file changed, 8 insertions(+), 49 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index aa296aace7..080ec5ed12 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -300,57 +300,16 @@ let add_and_check_ident id set =
   Id.Set.add id set
 
 let bound_glob_vars =
-  let rec vars bound = function
-    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c ->
-        let bound = name_fold add_and_check_ident na bound in
-        fold_glob_constr vars bound c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
-	let bound = vars_option bound rtntypopt in
-	let bound =
-          List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
-	List.fold_left vars_pattern bound pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
-	let bound = vars_return_type bound rtntyp in
-	let bound = vars bound b in
-	let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
-	vars bound c
-    | GIf (loc,c,rtntyp,b1,b2) ->
-	let bound = vars_return_type bound rtntyp in
-	let bound = vars bound c in
-	let bound = vars bound b1 in
-	vars bound b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bound = Array.fold_right Id.Set.add idl bound in
-	let vars_fix i bound fid =
-	  let bound =
-	    List.fold_left
-	      (fun bound (na,k,bbd,bty) ->
-		 let bound = vars_option bound bbd in
-		 let bound = vars bound bty in
-		 name_fold add_and_check_ident na bound
-	      )
-	      bound
-	      bl.(i)
-	  in
-	  let bound = vars bound tyl.(i) in
-	  vars bound bv.(i)
-	in
-	Array.fold_left_i vars_fix bound idl
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
-    | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
-
-  and vars_pattern bound (loc,idl,p,c) =
-    let bound = List.fold_right add_and_check_ident idl bound in
-    vars bound c
-
-  and vars_option bound = function None -> bound | Some p -> vars bound p
-
-  and vars_return_type bound (na,tyopt) =
-    let bound = name_fold add_and_check_ident na bound in
-    vars_option bound tyopt
+  let rec vars bound =
+    fold_glob_constr_with_binders
+      (fun id () -> bound := add_and_check_ident id !bound)
+      (fun () () -> vars bound)
+      () ()
   in
   fun rt ->
-    vars Id.Set.empty rt
+    let bound = ref Id.Set.empty in
+    vars bound rt;
+    !bound
 
 (** Mapping of names in binders *)
 
-- 
cgit v1.2.3


From e2a8edaf595827af82be67a90c0c5b22c987abe5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 22 Nov 2016 13:50:10 +0100
Subject: A refined solution to the beta-iota discrepancies between 8.4 and 8.5
 "refine".

There is a long story of commits trying to improve the compatibility
between 8.4 and 8.5 refine, as discussed in
https://github.com/coq/coq/pull/346.

ac9c5986b77bf4a783f2bd0ad571645694c960e1 add beta-iota in hypotheses and conclusion
8afac4f87d9d7e3add1c19485f475bd2207bfde7 remove beta-iota in hypotheses
08e87eb96ab67ead60d92394eec6066d9b52e55e re-add beta-iota in hypotheses
c9c54122d1d9493a965b483939e119d52121d5a6 re-remove beta-iota in hypotheses
9194180e2da0f7f9a2b2c7574bb7261cc69ead17 revert re-remove beta-iota in hypotheses
6bb352a6743c7332b9715ac15e95c806a58d101c re-re-remove beta-iota in hypotheses if <= 8.5
d8baa76d86eaa691a5386669596a6004bb44bb7a idem if = 8.5

The current commit tries to identify (one of?) the exact points of
divergence between 8.4 and 8.5 refine, namely the types inferred for
the variables of a pattern-matching problem.

Note that for the conclusion of each new goal, there were a
nf_betaiota in 8.4 done in function Evarutil.evars_to_metas, so the
compatibility expects that such a nf_betaiota on the conclusion of
each goal remains.
---
 pretyping/cases.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6bc2a4f94b..8a49cd5488 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1245,6 +1245,12 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   let typs = List.map2 RelDecl.set_name names cs_args
   in
 
+  (* Beta-iota-normalize types to better compatibility of refine with 8.4 behavior *)
+  (* This is a bit too strong I think, in the sense that what we would *)
+  (* really like is to have beta-iota reduction only at the positions where *)
+  (* parameters are substituted *)
+  let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in
+
   (* We build the matrix obtained by expanding the matching on *)
   (* "C x1..xn as x" followed by a residual matching on eqn into *)
   (* a matching on "x1 .. xn eqn" *)
-- 
cgit v1.2.3


From 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Apr 2017 16:30:45 +0200
Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with
 evars).

The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.

One day, evar kinds will need a little cleaning...
---
 pretyping/patternops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 2090aad8a0..75d3ed30ba 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -160,7 +160,9 @@ let pattern_of_constr env sigma t =
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
 	let () = ignore (pattern_of_constr env ty) in
         assert (not b); PMeta (Some id)
-      | Evar_kinds.GoalEvar -> 
+      | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
+        (* These are the two evar kinds used for existing goals *)
+        (* see Proofview.mark_in_evm *)
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
-- 
cgit v1.2.3


From db28e827d21658797418c320d566fb99570b44b6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:20:35 +0200
Subject: Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions
 with evars)."

One day I'll get bored of spending my nights fixing commits that were
pushed without being tested, and I'll ask for removal of push rights.
But for now let's pretend I haven't insisted enough:

~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~

Thank you!
---
 pretyping/patternops.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 75d3ed30ba..2090aad8a0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -160,9 +160,7 @@ let pattern_of_constr env sigma t =
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
 	let () = ignore (pattern_of_constr env ty) in
         assert (not b); PMeta (Some id)
-      | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
-        (* These are the two evar kinds used for existing goals *)
-        (* see Proofview.mark_in_evm *)
+      | Evar_kinds.GoalEvar -> 
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
-- 
cgit v1.2.3


From 12f1c409daf2cdbd7d0323f0d61723819532b362 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 16:56:25 +0200
Subject: Really fixing #2602 which was wrongly working because of #5487 hiding
 the cause.

The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
---
 pretyping/constr_matching.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3c47cfdc4b..afdf601c21 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -347,6 +347,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 
       |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
       |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst
+      | PEvar (c1,args1), Evar (c2,args2) when c1 = c2 ->
+         Array.fold_left2 (sorec ctx env) subst args1 args2
+
       | _ -> raise PatternMatchingFailure
 
   in
-- 
cgit v1.2.3


From c3aec655a8a33fff676c79e12888d193cc2e237b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 16:58:38 +0200
Subject: Fixing #5487 (v8.5 regression on ltac-matching expressions with
 evars).

The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.

One day, evar kinds will need a little cleaning...

PS: This is a second attempt, completing db28e82 which was missing the
case PEvar in constr_matching.ml. Indeed the attached fix to #5487
alone made #2602 failing, revealing that the real cause for #2602 was
actually not fixed and that if the test for #2602 was working it was
because of #5487 hiding the real problem in #2602.
---
 pretyping/patternops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 2090aad8a0..75d3ed30ba 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -160,7 +160,9 @@ let pattern_of_constr env sigma t =
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
 	let () = ignore (pattern_of_constr env ty) in
         assert (not b); PMeta (Some id)
-      | Evar_kinds.GoalEvar -> 
+      | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
+        (* These are the two evar kinds used for existing goals *)
+        (* see Proofview.mark_in_evm *)
 	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
 	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
-- 
cgit v1.2.3


From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 22:48:32 +0200
Subject: Allow flexible anonymous universes in instances and sorts.

The addition to the test suite showcases the usage.
---
 pretyping/detyping.ml  |  7 ++++--
 pretyping/miscops.ml   |  2 +-
 pretyping/pretyping.ml | 61 +++++++++++++++++++++++++++-----------------------
 3 files changed, 39 insertions(+), 31 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 483e2b4320..8a90a3f9bc 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -422,7 +422,9 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
+       then
+         let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in
+         [dl, Name.mk_name (Id.of_string_soft u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -434,7 +436,8 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
+  let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in
+  GType (Some (dl, Name.mk_name (Id.of_string_soft l)))
 
 let detype_instance sigma l = 
   let l = EInstance.kind sigma l in
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 7fe81c9a43..1669f8334b 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2
+| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 68ef976592..767e4be35b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -192,45 +192,50 @@ let _ =
 	    optwrite = (:=) Universes.set_minimization })
 						  
 (** Miscellaneous interpretation functions *)
-let interp_universe_level_name evd (loc,s) =
-  let names, _ = Global.global_universe_names () in
-    if CString.string_contains ~where:s ~what:"." then
-      match List.rev (CString.split '.' s) with
-      | [] -> anomaly (str"Invalid universe name " ++ str s)
-      | n :: dp -> 
-	 let num = int_of_string n in
-	 let dp = DirPath.make (List.map Id.of_string dp) in
-	 let level = Univ.Level.make dp num in
-	 let evd =
-	   try Evd.add_global_univ evd level
-	   with UGraph.AlreadyDeclared -> evd
-	 in evd, level
-    else 
-      try
-	let level = Evd.universe_of_name evd s in
-	evd, level
-      with Not_found ->
-	try 
-	  let id = try Id.of_string s with _ -> raise Not_found in
-          evd, snd (Idmap.find id names)
-	with Not_found -> 
-	  if not (is_strict_universe_declarations ()) then
-  	    new_univ_level_variable ~loc ~name:s univ_rigid evd
-	  else user_err ~loc ~hdr:"interp_universe_level_name"
-			     (Pp.(str "Undeclared universe: " ++ str s))
+let interp_universe_level_name ~anon_rigidity evd (loc,s) =
+  match s with
+  | Anonymous ->
+     new_univ_level_variable ~loc anon_rigidity evd
+  | Name s ->
+     let s = Id.to_string s in
+     let names, _ = Global.global_universe_names () in
+     if CString.string_contains ~where:s ~what:"." then
+       match List.rev (CString.split '.' s) with
+       | [] -> anomaly (str"Invalid universe name " ++ str s)
+       | n :: dp ->
+	  let num = int_of_string n in
+	  let dp = DirPath.make (List.map Id.of_string dp) in
+	  let level = Univ.Level.make dp num in
+	  let evd =
+	    try Evd.add_global_univ evd level
+	    with UGraph.AlreadyDeclared -> evd
+	  in evd, level
+     else
+       try
+	 let level = Evd.universe_of_name evd s in
+	 evd, level
+       with Not_found ->
+	 try
+	   let id = try Id.of_string s with _ -> raise Not_found in
+           evd, snd (Idmap.find id names)
+	 with Not_found ->
+	   if not (is_strict_universe_declarations ()) then
+  	     new_univ_level_variable ~loc ~name:s univ_rigid evd
+	   else user_err ~loc ~hdr:"interp_universe_level_name"
+		  (Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
 	    evd, Univ.Universe.make l
   | l ->
     List.fold_left (fun (evd, u) l -> 
-      let evd', l = interp_universe_level_name evd l in
+        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible_alg evd l in
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
 let interp_level_info loc evd : Misctypes.level_info -> _ = function
   | None -> new_univ_level_variable ~loc univ_rigid evd
-  | Some (loc,s) -> interp_universe_level_name evd (loc,s)
+  | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (loc,s)
 
 let interp_sort ?loc evd = function
   | GProp -> evd, Prop Null
-- 
cgit v1.2.3


From 4361c1ed9ac5646055f9f0eecc4a003d720c1994 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 12 Apr 2017 13:29:16 +0200
Subject: Type@{_} should not produce a flexible algebraic universe.

Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
---
 pretyping/pretyping.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 767e4be35b..4886423bd0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -229,7 +229,8 @@ let interp_universe ?loc evd = function
 	    evd, Univ.Universe.make l
   | l ->
     List.fold_left (fun (evd, u) l -> 
-        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible_alg evd l in
+        (* [univ_flexible_alg] can produce algebraic universes in terms *)
+        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
-- 
cgit v1.2.3


From 844bffb7d6c84a02dcef300dda9099487b23c09a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Apr 2017 21:17:03 +0200
Subject: Added an option Set Debug Cbv.

---
 pretyping/cbv.ml | 27 ++++++++++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index e18625c427..bd7350dc4e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -175,6 +175,19 @@ let cofixp_reducible flgs _ stk =
   else
     false
 
+let debug_cbv = ref false
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname = "cbv visited constants display";
+  Goptions.optkey = ["Debug";"Cbv"];
+  Goptions.optread = (fun () -> !debug_cbv);
+  Goptions.optwrite = (fun a -> debug_cbv:=a);
+}
+
+let pr_key = function
+  | ConstKey (sp,_) -> Names.Constant.print sp
+  | VarKey id -> Names.Id.print id
+  | RelKey n -> Pp.(str "REL_" ++ int n)
 
 (* The main recursive functions
  *
@@ -254,9 +267,17 @@ let rec norm_head info env t stack =
 and norm_head_ref k info env stack normt =
   if red_set_ref (info_flags info) normt then
     match ref_value_cache info normt with
-      | Some body -> strip_appl (shift_value k body) stack
-      | None -> (VAL(0,make_constr_ref k normt),stack)
-  else (VAL(0,make_constr_ref k normt),stack)
+      | Some body ->
+         if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
+         strip_appl (shift_value k body) stack
+      | None ->
+         if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+         (VAL(0,make_constr_ref k normt),stack)
+  else
+    begin
+      if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+      (VAL(0,make_constr_ref k normt),stack)
+    end
 
 (* cbv_stack_term performs weak reduction on constr t under the subs
  * env, with context stack, i.e. ([env]t stack).  First computes weak
-- 
cgit v1.2.3


From 7e28feadd6394483b6f527d5aed7d663e189596e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 23:26:44 +0200
Subject: Upgrading some local function as a general-purpose combinator
 Option.List.map.

---
 pretyping/evarsolve.ml | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f0d0114775..4ada91eb59 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -470,23 +470,13 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c =
 (* Managing pattern-unification *)
 (********************************)
 
-let map_all f l =
-  let rec map_aux f l = match l with
-  | [] -> []
-  | x :: l ->
-    match f x with
-    | None -> raise Exit
-    | Some y -> y :: map_aux f l
-  in
-  try Some (map_aux f l) with Exit -> None
-
 let expand_and_check_vars sigma aliases l =
   let map a = match get_alias_chain_of sigma aliases a with
   | None, [] -> Some a
   | None, a :: _ -> Some a
   | Some _, _ -> None
   in
-  map_all map l
+  Option.List.map map l
 
 let alias_distinct l =
   let rec check (rels, vars) = function
@@ -540,7 +530,7 @@ let is_unification_pattern_meta env evd nb m l t =
   | Rel n -> if n <= nb then Some (RelAlias n) else None
   | _ -> None
   in
-  match map_all map l with
+  match Option.List.map map l with
   | Some l ->
     begin match find_unification_pattern_args env evd l t with
     | Some _ as x when not (dependent evd (mkMeta m) t) -> x
@@ -550,10 +540,10 @@ let is_unification_pattern_meta env evd nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  match map_all (fun c -> to_alias evd c) l with
+  match Option.List.map (fun c -> to_alias evd c) l with
   | Some l when noccur_evar env evd evk t ->
     let args = remove_instance_local_defs evd evk args in
-    let args = map_all (fun c -> to_alias evd c) args in
+    let args = Option.List.map (fun c -> to_alias evd c) args in
     begin match args with
     | None -> None
     | Some args ->
-- 
cgit v1.2.3


From e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 May 2017 18:12:55 +0200
Subject: Remove dead code and unused open.

---
 pretyping/glob_ops.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 080ec5ed12..6509aaac3d 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -266,11 +266,6 @@ let occur_glob_constr id =
        fold_glob_constr_with_binders g f barred acc c in
   occur false false
 
-let add_name_to_ids set na =
-  match na with
-    | Anonymous -> set
-    | Name id -> Id.Set.add id set
-
 let free_glob_vars =
   let rec vars bound vs = function
     | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs
-- 
cgit v1.2.3


From 3908fb1c6d68678daa65b4a2fa944424575acf87 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 14 May 2017 12:29:33 +0200
Subject: Removing a line warned unused.

---
 pretyping/constr_matching.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index afdf601c21..daac33f503 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -84,7 +84,6 @@ let rec build_lambda vars ctx m = match vars with
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
-  let len = List.length ctx in
   let pre, suf = List.chop (pred n) ctx in
   let (na, t, suf) = match suf with
   | [] -> assert false
-- 
cgit v1.2.3