Merge branch 'trunk' into located_switch

31 files changed, 227 insertions, 271 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3beef77731..e7b17991e3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1246,6 +1246,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" *)
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
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index b014af2c7f..eb25994bef 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open CClosure
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index e9b3d197bc..32da81f96c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -17,7 +17,6 @@ open Nametab
 open Environ
 open Libobject
 open Term
-open Termops
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 0d741a5a5d..c4238e8b0d 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open EConstr
 open Evd
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index a93653f32e..98a00f4332 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -22,7 +22,6 @@ open Environ
 open EConstr
 open Vars
 open Reductionops
-open Typeops
 open Pretype_errors
 open Classops
 open Evarutil
@@ -480,8 +479,8 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 =
           (* We eta-expand (hence possibly modifying the original term!) *)
 	  (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
 	  (* has type forall (x:u1), u2 (with v' recursively obtained) *)
-          (* Note: we retype the term because sort-polymorphism may have *)
-          (* weaken its type *)
+          (* Note: we retype the term because template polymorphism may have *)
+          (* weakened its type *)
 	  let name = match name with
 	    | Anonymous -> Name Namegen.default_dependent_ident
 	    | _ -> name in
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 25ee82bbf1..ab1f6c110f 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -8,7 +8,6 @@
 
 open Evd
 open Names
-open Term
 open Environ
 open EConstr
 open Glob_term
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index efe03bc2e9..edcfa99c86 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -83,32 +83,70 @@ let add_binders na1 na2 binding_vars (names, terms as subst) =
 
 let rec build_lambda sigma vars ctx m = match vars with
 | [] ->
-  let len = List.length ctx in
-  EConstr.Vars.lift (-1 * len) m
+  if Vars.closed0 sigma m then m else raise PatternMatchingFailure
 | n :: vars ->
-  let open EConstr in
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
-  let len = List.length ctx in
-  let init i =
-    if i < pred n then mkRel (i + 2)
-    else if Int.equal i (pred n) then mkRel 1
-    else mkRel (i + 1)
-  in
-  let m = Vars.substl (List.init len init) m in
   let pre, suf = List.chop (pred n) ctx in
-  match suf with
+  let (na, t, suf) = match suf with
   | [] -> assert false
-  | (_, na, t) :: suf ->
-    let map i = if i > n then pred i else i in
-    let vars = List.map map vars in
-    (** Check that the abstraction is legal *)
-    let frels = free_rels sigma t in
-    let brels = List.fold_right Int.Set.add vars Int.Set.empty in
-    let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in
-    (** Create the abstraction *)
-    let m = mkLambda (na, t, m) in
-    build_lambda sigma vars (pre @ suf) m
+  | (_, na, t) :: suf -> (na, t, suf)
+  in
+  (** Check that the abstraction is legal by generating a transitive closure of
+      its dependencies. *)
+  let is_nondep t clear = match clear with
+  | [] -> true
+  | _ ->
+    let rels = free_rels sigma t in
+    let check i b = b || not (Int.Set.mem i rels) in
+    List.for_all_i check 1 clear
+  in
+  let fold (_, _, t) clear = is_nondep t clear :: clear in
+  (** Produce a list of booleans: true iff we keep the hypothesis *)
+  let clear = List.fold_right fold pre [false] in
+  let clear = List.drop_last clear in
+  (** If the conclusion depends on a variable we cleared, failure *)
+  let () = if not (is_nondep m clear) then raise PatternMatchingFailure in
+  (** Create the abstracted term *)
+  let fold (k, accu) keep =
+    if keep then
+      let k = succ k in
+      (k, Some k :: accu)
+    else (k, None :: accu)
+  in
+  let keep, shift = List.fold_left fold (0, []) clear in
+  let shift = List.rev shift in
+  let map = function
+  | None -> mkProp (** dummy term *)
+  | Some i -> mkRel (i + 1)
+  in
+  (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *)
+  let subst =
+    List.map map shift @
+    mkRel 1 ::
+    List.mapi (fun i _ -> mkRel (i + keep + 2)) suf
+  in
+  let map i (id, na, c) =
+    let i = succ i in
+    let subst = List.skipn i subst in
+    let subst = List.map (fun c -> Vars.lift (- i) c) subst in
+    (id, na, substl subst c)
+  in
+  let pre = List.mapi map pre in
+  let pre = List.filter_with clear pre in
+  let m = substl subst m in
+  let map i =
+    if i > n then i - n + keep
+    else match List.nth shift (i - 1) with
+    | None ->
+      (** We cleared a variable that we wanted to abstract! *)
+      raise PatternMatchingFailure
+    | Some k -> k
+  in
+  let vars = List.map map vars in
+  (** Create the abstraction *)
+  let m = mkLambda (na, Vars.lift keep t, m) in
+  build_lambda sigma vars (pre @ suf) m
 
 let rec extract_bound_aux k accu frels ctx = match ctx with
 | [] -> accu
@@ -323,6 +361,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 
       |	PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst
       |	PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
+      | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
+         Array.fold_left2 (sorec ctx env) subst args1 args2
       | _ -> raise PatternMatchingFailure
 
   in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2bfd67f6f3..92359420e9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -13,7 +13,6 @@ open CErrors
 open Util
 open Names
 open Term
-open Environ
 open EConstr
 open Vars
 open Inductiveops
@@ -421,7 +420,9 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [Loc.tag @@ 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
+         [Loc.tag @@ Name.mk_name (Id.of_string_soft u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -433,7 +434,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 (Loc.tag @@ 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 (Loc.tag @@ Name.mk_name (Id.of_string_soft l)))
 
 let detype_instance sigma l = 
   let l = EInstance.kind sigma l in
@@ -694,7 +696,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
       let c = detype (lax,false) avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
       let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
-      let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in
+      let t = if s != InProp  && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in
       GLetIn (na', c, t, r)
 
 let detype_rel_context ?(lax=false) where avoid env sigma sign =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1318942c58..6fcbaa8ef5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -21,7 +21,6 @@ open Recordops
 open Evarutil
 open Evardefine
 open Evarsolve
-open Globnames
 open Evd
 open Pretype_errors
 open Sigma.Notations
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index fc07f0fbea..7cee1e8a7e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open EConstr
 open Environ
 open Reductionops
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index c2b267dd8e..a116198465 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -11,7 +11,6 @@ open Pp
 open Names
 open Term
 open Termops
-open Environ
 open EConstr
 open Vars
 open Namegen
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 77086d046c..4ada91eb59 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
 open Util
 open CErrors
 open Names
@@ -471,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
@@ -541,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
@@ -551,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 ->
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index e3d3b74f10..d22f94e4e5 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Locus
-open Term
 open Evd
 open Pretype_errors
 open Environ
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 94bc24e3c0..923d7d9388 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -214,121 +214,64 @@ let fold_glob_constr f acc = CAst.with_val (function
   | (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 same_id na id = match na with
-| Anonymous -> false
-| Name id' -> Id.equal id id'
+let fold_glob_constr_with_binders g f v acc = CAst.(with_val (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 iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
 let occur_glob_constr id =
-  let rec occur gt = CAst.with_val (function
-    | GVar (id') -> Id.equal id id'
-    | GApp (f,args) -> (occur f) || (List.exists occur args)
-    | GLambda (na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GProd (na,bk,ty,c) ->
-      (occur ty) || (not (same_id na id) && (occur c))
-    | GLetIn (na,b,t,c) ->
-      (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
-    | GCases (sty,rtntypopt,tml,pl) ->
-	(occur_option rtntypopt)
-        || (List.exists (fun (tm,_) -> occur tm) tml)
-	|| (List.exists occur_pattern pl)
-    | GLetTuple (nal,rtntyp,b,c) ->
-	occur_return_type rtntyp id
-        || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c))
-    | GIf (c,rtntyp,b1,b2) ->
-	occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
-    | GRec (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 (c,k) -> (occur c) || (match k with CastConv t
-      | CastVM t | CastNative t -> occur t | CastCoerce -> false)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
-    ) gt
-  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
-
-
-let add_name_to_ids set na =
-  match na with
-    | Anonymous -> set
-    | Name id -> Id.Set.add id set
+  let open CAst in
+  let rec occur barred acc = function
+    | { loc ; v = GVar id' } -> Id.equal id id'
+    | 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 free_glob_vars =
-  let rec vars bounded vs = CAst.with_val @@ (function
-    | GVar (id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
-    | GApp (f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | GLambda (na,_,ty,c) | GProd (na,_,ty,c) ->
-	let vs' = vars bounded vs ty in
-	let bounded' = add_name_to_ids bounded na in
-       vars bounded' vs' c
-    | GLetIn (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 (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 (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 (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 (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 (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 open CAst in
+  let rec vars bound vs = function
+    | { loc ; v = GVar 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
@@ -354,57 +297,16 @@ let add_and_check_ident id set =
   Id.Set.add id set
 
 let bound_glob_vars =
-  let rec vars bound c = match c.CAst.v with
-    | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) ->
-        let bound = name_fold add_and_check_ident na bound in
-        fold_glob_constr vars bound c
-    | GCases (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 (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 (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 (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 _ -> 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 *)
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index dae662747f..aa48516aff 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
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5b42add285..429e5005ec 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -459,7 +459,6 @@ let extract_mrectype sigma t =
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let open EConstr in
   let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index f53677abbb..69bc2d11ff 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/patternops.ml b/pretyping/patternops.ml
index 1884b69279..a8012d35f8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -14,13 +14,11 @@ open Nameops
 open Term
 open Vars
 open Glob_term
-open Glob_ops
 open Pp
 open Mod_subst
 open Misctypes
 open Decl_kinds
 open Pattern
-open Evd
 open Environ
 
 let case_info_pattern_eq i1 i2 =
@@ -156,12 +154,15 @@ let pattern_of_constr env sigma t =
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
       pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
-    | Evar (evk,ctxt) ->
+    | Evar (evk,ctxt as ev) ->
       (match snd (Evd.evar_source evk sigma) with
       | Evar_kinds.MatchingVar (b,id) ->
         assert (not b); PMeta (Some id)
-      | Evar_kinds.GoalEvar -> 
-	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+      | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
+        (* These are the two evar kinds used for existing goals *)
+        (* see Proofview.mark_in_evm *)
+         if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
+         else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
       | _ -> 
 	 PMeta None)
     | Case (ci,p,a,br) ->
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 5694d345c1..791fd74ed3 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Globnames
 open Glob_term
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ef187e7a63..d7c04b08b0 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 76df89a264..53df5aa4a5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -33,7 +33,6 @@ open EConstr
 open Vars
 open Reductionops
 open Type_errors
-open Typeops
 open Typing
 open Globnames
 open Nameops
@@ -191,47 +190,53 @@ let _ =
 	    optkey   = ["Universe";"Minimization";"ToSet"];
 	    optread  = Universes.is_set_minimization;
 	    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 s "." 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
+        (* [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
 
 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.tag ?loc s)
 
 let interp_sort ?loc evd = function
   | GProp -> evd, Prop Null
@@ -540,17 +545,17 @@ let pretype_ref ?loc evdref env ref us =
     let ty = unsafe_type_of env.ExtraEnv.env evd c in
       make_judge c ty
 
-let judge_of_Type loc evd s =
+let judge_of_Type ?loc evd s =
   let evd, s = interp_universe ?loc evd s in
   let judge = 
     { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
   in
     evd, judge
 
-let pretype_sort loc evdref = function
+let pretype_sort ?loc evdref = function
   | GProp -> judge_of_prop
   | GSet -> judge_of_set
-  | GType s -> evd_comb1 (judge_of_Type loc) evdref s
+  | GType s -> evd_comb1 (judge_of_Type ?loc) evdref s
 
 let new_type_evar env evdref loc =
   let sigma = Sigma.Unsafe.of_evar_map !evdref in
@@ -713,7 +718,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	inh_conv_coerce_to_tycon ?loc env evdref fixj tycon
 
   | GSort s ->
-    let j = pretype_sort loc evdref s in
+    let j = pretype_sort ?loc evdref s in
       inh_conv_coerce_to_tycon ?loc env evdref j tycon
 
   | GApp (f,args) ->
diff --git a/pretyping/program.ml b/pretyping/program.ml
index caa5a5c8a6..42acc5705b 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2703205386..52f424f751 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -239,6 +239,9 @@ sig
   | Shift of int
   | Update of 'a
   and 'a t = 'a member list
+
+  exception IncompatibleFold2
+
   val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
   val empty : 'a t
   val is_empty : 'a t -> bool
@@ -413,6 +416,7 @@ struct
       | (_,_) -> false in
     compare_rec 0 stk1 stk2
 
+  exception IncompatibleFold2
   let fold2 f o sk1 sk2 =
     let rec aux o lft1 sk1 lft2 sk2 =
       let fold_array =
@@ -442,7 +446,7 @@ struct
 	  aux o lft1 (List.rev params1) lft2 (List.rev params2)
 	in aux o' lft1' q1 lft2' q2
       | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
-	raise (Invalid_argument "Reductionops.Stack.fold2")
+	raise IncompatibleFold2
     in aux o 0 (List.rev sk1) 0 (List.rev sk2)
 
   let rec map f x = List.map (function
@@ -1117,7 +1121,9 @@ let local_whd_state_gen flags sigma =
   whrec
 
 let raw_whd_state_gen flags env =
-  let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in
+  let f sigma s = fst (whd_state_gen ~refold:(get_refolding_in_reduction ())
+                         ~tactic_mode:false
+                         flags env sigma s) in
   f
 
 let stack_red_of_state_red f =
@@ -1127,7 +1133,7 @@ let stack_red_of_state_red f =
 (* Drops the Cst_stack *)
 let iterate_whd_gen refold flags env sigma s =
   let rec aux t =
-  let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
+  let (hd,sk),_ = whd_state_gen ~refold ~tactic_mode:false flags env sigma (t,Stack.empty) in
   let whd_sk = Stack.map aux sk in
   Stack.zip sigma ~refold (hd,whd_sk)
   in aux s
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 752c30a8ac..af80481569 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -81,8 +81,11 @@ module Stack : sig
   val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
 
   val compare_shape : 'a t -> 'a t -> bool
+
+  exception IncompatibleFold2
   (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
-      @return the result and the lifts to apply on the terms *)
+      @return the result and the lifts to apply on the terms
+      @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *)
   val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
     constr t -> constr t -> 'a * int * int
   val map : ('a -> 'a) -> 'a t -> 'a t
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 76d0bc241f..c31212e26a 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Term
 open Environ
 open Evd
 open EConstr
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 2db0e9e881..754dacd193 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -8,7 +8,6 @@
 
 (*i*)
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 9bd430e4d6..558575ccce 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -8,7 +8,6 @@
 
 open Loc
 open Names
-open Term
 open EConstr
 open Environ
 open Constrexpr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 41d994553f..757e12451e 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -313,14 +313,13 @@ let rec execute env evdref cstr =
 	let j =
 	  match EConstr.kind !evdref f with
 	    | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
-		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env !evdref (ind, u) jl)
 	    | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env ->
-		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env !evdref (cst, u) jl)
 	    | _ ->
+                (* No template polymorphism *)
 		execute env evdref f
 	in
 	e_judge_of_apply env evdref j jl
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9678e3a429..74fbd2a851 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1095,7 +1095,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       let app = mkApp (c, Array.rev_of_list ks) in
       (* let substn = unirec_rec curenvnb pb b false substn t cN in *)
 	unirec_rec curenvnb pb opt' substn c1 app
-      with Invalid_argument "Reductionops.Stack.fold2" ->
+      with Reductionops.Stack.IncompatibleFold2 ->
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
   in
@@ -1535,9 +1535,6 @@ let indirectly_dependent sigma c d decls =
        way to see that the second hypothesis depends indirectly over 2 *)
     List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
 
-let indirect_dependency sigma d decls =
-  decls  |>  List.filter (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d)  |>  List.hd  |>  NamedDecl.get_id
-
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let current_sigma = Sigma.to_evar_map current_sigma in
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 148178f2fc..8d7e3521d6 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -45,7 +45,7 @@ val elim_no_delta_flags : unit -> unify_flags
 
 val is_keyed_unification : unit -> bool
 
-(** The "unique" unification fonction *)
+(** The "unique" unification function *)
 val w_unify :
   env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map