Merge branch 'trunk' into located_switch

10 files changed, 70 insertions, 103 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bb9075e74..54d3ce6cf 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open CSig
 open CErrors
 open Util
 open Names
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 3a9469e55..693b592fd 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -9,7 +9,6 @@
 open CSig
 open Names
 open Constr
-open Context
 open Environ
 
 type t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ac64ab834..6cba6f607 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Names
 open Term
-open Vars
 open Termops
 open Namegen
 open Pre_env
@@ -462,7 +461,7 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
   ev
 
 (* This assumes an evar with identity instance and generalizes it over only
-   the De Bruijn part of the context *)
+   the de Bruijn part of the context *)
 let generalize_evar_over_rels sigma (ev,args) =
   let open EConstr in
   let evi = Evd.find sigma ev in
diff --git a/engine/evd.ml b/engine/evd.ml
index b0531d581..8ade6cb99 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -14,10 +14,8 @@ open Nameops
 open Term
 open Vars
 open Environ
-open Globnames
-open Context.Named.Declaration
 
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
 (** Generic filters *)
@@ -360,8 +358,6 @@ module EvMap = Evar.Map
 module EvNames :
 sig
 
-open Misctypes
-
 type t
 
 val empty : t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 84bcecc44..7f80d40d6 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -858,14 +858,12 @@ let tclPROGRESS t =
   let quick_test =
     initial.solution == final.solution && initial.comb == final.comb
   in
-  let exhaustive_test =
+  let test =
+    quick_test ||
     Util.List.for_all2eq begin fun i f ->
       Progress.goal_equal initial.solution i final.solution f
     end initial.comb final.comb
   in
-  let test =
-    quick_test || exhaustive_test
-  in
   if not test then
     tclUNIT res
   else
diff --git a/engine/proofview.mli b/engine/proofview.mli
index a3b0304b1..da8a8fecd 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -13,7 +13,6 @@
     state and returning a value of type ['a]. *)
 
 open Util
-open Term
 open EConstr
 
 (** Main state of tactics *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 64f4c6dc5..19e62f8e6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -612,30 +612,6 @@ let adjust_app_array_size f1 l1 f2 l2 =
     let extras,restl1 = Array.chop (len1-len2) l1 in
     (mkApp (f1,extras), restl1, f2, l2)
 
-(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
-   subterms of [c]; it carries an extra data [l] (typically a name
-   list) which is processed by [g na] (which typically cons [na] to
-   [l]) at each binder traversal (with name [na]); it is not recursive
-   and the order with which subterms are processed is not specified *)
-
-let map_constr_with_named_binders g f l c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (c,k,t) -> mkCast (f l c, k, f l t)
-  | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c)
-  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
-  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
-  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
-  | Proj (p,c) -> mkProj (p, f l c)
-  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
-  | Fix (ln,(lna,tl,bl)) ->
-      let l' = Array.fold_left (fun l na -> g na l) l lna in
-      mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-  | CoFix(ln,(lna,tl,bl)) ->
-      let l' = Array.fold_left (fun l na -> g na l) l lna in
-      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-
 (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
    immediate subterms of [c]; it carries an extra data [n] (typically
    a lift index) which is processed by [g] (which typically add 1 to
@@ -1451,7 +1427,6 @@ let dependency_closure env sigma sign hyps =
     List.rev lh
 
 let global_app_of_constr sigma c =
-  let open Univ in
   let open Globnames in
   match EConstr.kind sigma c with
   | Const (c, u) -> (ConstRef c, u), None
diff --git a/engine/uState.ml b/engine/uState.ml
index eb1acb845..dc6822057 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -131,84 +131,87 @@ let instantiate_variable l b v =
 exception UniversesDiffer
 
 let process_universe_constraints ctx cstrs =
+  let open Univ in
   let univs = ctx.uctx_universes in
   let vars = ref ctx.uctx_univ_variables in
   let normalize = Universes.normalize_universe_opt_subst vars in
-  let rec unify_universes fo l d r local =
+  let is_local l = Univ.LMap.mem l !vars in
+  let varinfo x =
+    match Univ.Universe.level x with
+    | None -> Inl x
+    | Some l -> Inr l
+  in
+  let equalize_variables fo l l' r r' local =
+    (** Assumes l = [l',0] and r = [r',0] *)
+    let () =
+      if is_local l' then
+        instantiate_variable l' r vars
+      else if is_local r' then
+        instantiate_variable r' l vars
+      else if not (UGraph.check_eq_level univs l' r') then
+        (* Two rigid/global levels, none of them being local,
+            one of them being Prop/Set, disallow *)
+        if Univ.Level.is_small l' || Univ.Level.is_small r' then
+          raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+        else if fo then
+          raise UniversesDiffer
+    in
+    Univ.enforce_eq_level l' r' local
+  in
+  let equalize_universes l r local = match varinfo l, varinfo r with
+  | Inr l', Inr r' -> equalize_variables false l l' r r' local
+  | Inr l, Inl r | Inl r, Inr l ->
+    let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in
+    let inst = Univ.univ_level_rem l r r in
+      if alg then (instantiate_variable l inst vars; local)
+      else
+        let lu = Univ.Universe.make l in
+        if Univ.univ_level_mem l r then
+          Univ.enforce_leq inst lu local
+        else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+  | Inl _, Inl _ (* both are algebraic *) ->
+    if UGraph.check_eq univs l r then local
+    else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+  in
+  let unify_universes (l, d, r) local =
     let l = normalize l and r = normalize r in
       if Univ.Universe.equal l r then local
       else 
-        let varinfo x = 
-          match Univ.Universe.level x with
-          | None -> Inl x
-          | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic)
-        in
-          if d == Universes.ULe then
+          match d with
+          | Universes.ULe ->
             if UGraph.check_leq univs l r then
               (** Keep Prop/Set <= var around if var might be instantiated by prop or set
                   later. *)
-              if Univ.Universe.is_level l then 
-                match Univ.Universe.level r with
-                | Some r ->
-                  Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
-                | _ -> local
-              else local
+              match Univ.Universe.level l, Univ.Universe.level r with
+              | Some l, Some r ->
+                Univ.Constraint.add (l, Univ.Le, r) local
+              | _ -> local
             else
-              match Univ.Universe.level r with
+              begin match Univ.Universe.level r with
               | None -> error ("Algebraic universe on the right")
-              | Some rl ->
-                if Univ.Level.is_small rl then
+              | Some r' ->
+                if Univ.Level.is_small r' then
                   let levels = Univ.Universe.levels l in
-                    Univ.LSet.fold (fun l local ->
-                      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
-                        unify_universes fo (Univ.Universe.make l) Universes.UEq r local
-                      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
-                      levels local
+                  let fold l' local =
+                    let l = Univ.Universe.make l' in
+                    if Univ.Level.is_small l' || is_local l' then
+                      equalize_variables false l l' r r' local
+                    else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None))
+                  in
+                  Univ.LSet.fold fold levels local
                 else
                   Univ.enforce_leq l r local
-          else if d == Universes.ULub then
-            match varinfo l, varinfo r with
-            | (Inr (l, true, _), Inr (r, _, _)) 
-            | (Inr (r, _, _), Inr (l, true, _)) -> 
-              instantiate_variable l (Univ.Universe.make r) vars; 
-              Univ.enforce_eq_level l r local
-            | Inr (_, _, _), Inr (_, _, _) ->
-              unify_universes true l Universes.UEq r local
+              end
+          | Universes.ULub ->
+            begin match Universe.level l, Universe.level r with
+            | Some l', Some r' ->
+              equalize_variables true l l' r r' local
             | _, _ -> assert false
-          else (* d = Universes.UEq *)
-            match varinfo l, varinfo r with
-            | Inr (l', lloc, _), Inr (r', rloc, _) ->
-              let () = 
-                if lloc then
-                  instantiate_variable l' r vars
-                else if rloc then 
-                  instantiate_variable r' l vars
-                else if not (UGraph.check_eq univs l r) then
-                  (* Two rigid/global levels, none of them being local,
-                     one of them being Prop/Set, disallow *)
-                  if Univ.Level.is_small l' || Univ.Level.is_small r' then
-                    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
-                  else
-                    if fo then 
-                      raise UniversesDiffer
-              in
-                Univ.enforce_eq_level l' r' local
-            | Inr (l, loc, alg), Inl r
-            | Inl r, Inr (l, loc, alg) ->
-               let inst = Univ.univ_level_rem l r r in
-                 if alg then (instantiate_variable l inst vars; local)
-                 else
-                   let lu = Univ.Universe.make l in
-                   if Univ.univ_level_mem l r then
-                     Univ.enforce_leq inst lu local
-                   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
-            | _, _ (* One of the two is algebraic or global *) -> 
-             if UGraph.check_eq univs l r then local
-             else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+            end
+          | Universes.UEq -> equalize_universes l r local
   in
   let local = 
-    Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
-      cstrs Univ.Constraint.empty
+    Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty
   in
     !vars, local
 
diff --git a/engine/universes.ml b/engine/universes.ml
index ad5ff827b..1900112dd 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -13,7 +13,6 @@ open Term
 open Environ
 open Univ
 open Globnames
-open Decl_kinds
 
 let pr_with_global_universes l = 
   try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ())))
@@ -732,7 +731,7 @@ let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cs
 
 type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
 
-let pr_constraints_map cmap =
+let _pr_constraints_map (cmap:constraints_map) =
   LMap.fold (fun l cstrs acc -> 
     Level.pr l ++ str " => " ++ 
       prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
diff --git a/engine/universes.mli b/engine/universes.mli
index 932de941a..83ca1ea60 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -223,7 +223,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s
 
 val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
 
-(** {6 Support for old-style sort-polymorphism } *)
+(** {6 Support for template polymorphism } *)
 
 val solve_constraints_system : universe option array -> universe array -> universe array ->
   universe array