Merge PR #1109: Handle some misc todos

9 files changed, 44 insertions, 93 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 9055dcc86..96e4b6acc 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -31,7 +31,7 @@ open Environ
 (** {6 Evars} *)
 
 type evar = existential_key
-(** Existential variables. TODO: Should be made opaque one day. *)
+(** Existential variables. *)
 
 val string_of_existential : evar -> string
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d2b41aae9..8568bf14b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -166,16 +166,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       let mb_mp1 = lookup_module mp1 env in
       let mtb_mp1 = module_type_of_module mb_mp1 in
       let cst = match old.mod_expr with
-	| Abstract ->
-	  begin
-            try
-              let mtb_old = module_type_of_module old in
-              let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
-              Univ.ContextSet.add_constraints chk_cst old.mod_constraints
-	    with Failure _ ->
-              (* TODO: where can a Failure come from ??? *)
-              error_incorrect_with_constraint lab
-	  end
+        | Abstract ->
+          let mtb_old = module_type_of_module old in
+          let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
+          Univ.ContextSet.add_constraints chk_cst old.mod_constraints
 	| Algebraic (NoFunctor (MEident(mp'))) ->
 	  check_modpath_equiv env' mp1 mp';
 	  old.mod_constraints
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 044877e82..b40badd7c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -65,6 +65,10 @@ let type_of_type u =
   let uu = Universe.super u in
     mkType uu
 
+let type_of_sort = function
+  | Prop c -> type1
+  | Type u -> type_of_type u
+
 (*s Type of a de Bruijn index. *)
 
 let type_of_relative env n =
@@ -323,11 +327,7 @@ let rec execute env cstr =
   let open Context.Rel.Declaration in
   match kind_of_term cstr with
     (* Atomic terms *)
-    | Sort (Prop c) ->
-      type1
-	
-    | Sort (Type u) ->
-      type_of_type u
+    | Sort s -> type_of_sort s
 
     | Rel n ->
       type_of_relative env n
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a8f7fba9a..96be6c14a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -37,15 +37,19 @@ val assumption_of_judgment :  env -> unsafe_judgment -> types
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
 
 (** {6 Type of sorts. } *)
+val type1 : types
+val type_of_sort : Sorts.t -> types
 val judge_of_prop : unsafe_judgment
 val judge_of_set  : unsafe_judgment
 val judge_of_prop_contents  : contents -> unsafe_judgment
 val judge_of_type           : universe -> unsafe_judgment
 
 (** {6 Type of a bound variable. } *)
+val type_of_relative : env -> int -> types
 val judge_of_relative : env -> int -> unsafe_judgment
 
 (** {6 Type of variables } *)
+val type_of_variable : env -> variable -> types
 val judge_of_variable : env -> variable -> unsafe_judgment
 
 (** {6 type of a constant } *)
@@ -66,9 +70,9 @@ val judge_of_abstraction :
   env -> Name.t -> unsafe_type_judgment -> unsafe_judgment
     -> unsafe_judgment
 
-val sort_of_product : env -> sorts -> sorts -> sorts
-
 (** {6 Type of a product. } *)
+val sort_of_product : env -> sorts -> sorts -> sorts
+val type_of_product : env -> Name.t -> sorts -> sorts -> types
 val judge_of_product :
   env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment
     -> unsafe_judgment
diff --git a/man/coqdep.1 b/man/coqdep.1
index 81f7e1e0d..ed727db7c 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -82,7 +82,7 @@ Prints the dependencies of Caml modules.
 \" the standard output. No dependency is computed with this option.
 .TP 
 .BI \-I/\-Q/\-R \ options
-Have the same effects on load path and modules names than for other
+Have the same effects on load path and modules names as for other
 coq commands (coqtop, coqc).
 .TP 
 .BI \-coqlib \ directory
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 39c2ceeba..1038945c1 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -5,13 +5,11 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Pp
 open CErrors
 open Term
 open Vars
 open Environ
 open Reduction
-open Univ
 open Declarations
 open Names
 open Inductive
@@ -20,8 +18,6 @@ open Nativecode
 open Nativevalues
 open Context.Rel.Declaration
 
-module RelDecl = Context.Rel.Declaration
-
 (** This module implements normalization by evaluation to OCaml code *)
 
 exception Find_at of int
@@ -177,44 +173,6 @@ let build_case_type dep p realargs c =
   if dep then mkApp(mkApp(p, realargs), [|c|])
   else mkApp(p, realargs)
 
-(* TODO move this function *)
-let type_of_rel env n =
-  env |> lookup_rel n |> RelDecl.get_type |> lift n
-
-let type_of_prop = mkSort type1_sort
-
-let type_of_sort s = 
-  match s with
-  | Prop _ -> type_of_prop
-  | Type u -> mkType (Univ.super u)
-
-let type_of_var env id =
-  let open Context.Named.Declaration in
-  try env |> lookup_named id |> get_type
-  with Not_found ->
-    anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.")
-
-let sort_of_product env domsort rangsort =
-  match (domsort, rangsort) with
-    (* Product rule (s,Prop,Prop) *)
-    | (_,       Prop Null)  -> rangsort
-    (* Product rule (Prop/Set,Set,Set) *)
-    | (Prop _,  Prop Pos) -> rangsort
-    (* Product rule (Type,Set,?) *)
-    | (Type u1, Prop Pos) ->
-        if is_impredicative_set env then
-          (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
-          rangsort
-        else
-          (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (sup u1 type0_univ)
-    (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
-    (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Null, Type _)  -> rangsort
-    (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (sup u1 u2)
-
 (* normalisation of values *)
 
 let branch_of_switch lvl ans bs = 
@@ -328,15 +286,15 @@ and nf_atom_type env sigma atom =
   match atom with
   | Arel i ->
       let n = (nb_rel env - i) in
-      mkRel n, type_of_rel env n
+      mkRel n, Typeops.type_of_relative env n
   | Aconstant cst ->
       mkConstU cst, Typeops.type_of_constant_in env cst
   | Aind ind ->
       mkIndU ind, Inductiveops.type_of_inductive env ind
   | Asort s ->
-      mkSort s, type_of_sort s
+      mkSort s, Typeops.type_of_sort s
   | Avar id ->
-      mkVar id, type_of_var env id
+      mkVar id, Typeops.type_of_variable env id
   | Acase(ans,accu,p,bs) ->
       let a,ta = nf_accu_type env sigma accu in
       let ((mind,_),u as ind),allargs = find_rectype_a env ta in
@@ -387,7 +345,7 @@ and nf_atom_type env sigma atom =
       let vn = mk_rel_accu (nb_rel env) in
       let env = push_rel (LocalAssum (n,dom)) env in
       let codom,s2 = nf_type_sort env sigma (codom vn) in
-      mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
+      mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
   | Aevar(ev,ty) ->
      let ty = nf_type env sigma ty in
      mkEvar ev, ty
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 079524f34..56f8b33e0 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -214,7 +214,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
           type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty
     | Const (cst, u) ->
         let t = constant_type_in env (cst, EInstance.kind sigma u) in
-        (* TODO *)
           sigma, EConstr.of_constr t
     | Var id -> sigma, type_of_var env id
     | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index f80cb7cc6..4f575ab4b 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -110,10 +110,6 @@ module Strict = struct
   let push (b:t) pr =
     focus bullet_cond (b::get_bullets pr) 1 pr
 
-  (* Used only in the next function.
-     TODO: use a recursive function instead? *)
-  exception SuggestFound of t
-
   let suggest_bullet (prf : proof): suggestion =
     if is_done prf then ProofFinished
     else if not (no_focused_goal prf)
@@ -122,24 +118,24 @@ module Strict = struct
       | b::_ -> Unfinished b
       | _ -> NoBulletInUse
     else (* There is no goal under focus but some are unfocussed,
-            let us look at the bullet needed. If no  *)
-      let pcobaye = ref prf in
-      try
-        while true do
-          let pcobaye', b = pop !pcobaye in
-         (* pop went well, this means that there are no more goals
-          *under this* bullet b, see if a new b can be pushed. *)
-          (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
-      	 raise (SuggestFound b)
-           with SuggestFound _ as e -> raise e
-           | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
-          pcobaye := pcobaye'
-        done;
-        assert false
-      with SuggestFound b -> Suggest b
-      | _ -> NeedClosingBrace (* No push was possible, but there are still
-      			   subgoals somewhere: there must be a "}" to use. *)
-
+            let us look at the bullet needed. *)
+      let rec loop prf =
+        match pop prf with
+        | prf, b ->
+          (* pop went well, this means that there are no more goals
+           *under this* bullet b, see if a new b can be pushed. *)
+          begin
+            try ignore (push b prf); Suggest b
+            with _ ->
+              (* b could not be pushed, so we must look for a outer bullet *)
+              loop prf
+          end
+        | exception _ ->
+          (* No pop was possible, but there are still
+             subgoals somewhere: there must be a "}" to use. *)
+          NeedClosingBrace
+      in
+      loop prf
 
   let rec pop_until (prf : proof) bul : proof =
     let prf', b = pop prf in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d6c24e9cc..6f7e61f6b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1579,11 +1579,11 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in
   let hypmv =
-    try match List.remove Int.equal indmv (clenv_independent elimclause) with
-      | [a] -> a
-      | _ -> failwith ""
-    with Failure _ -> user_err ~hdr:"elimination_clause"
-          (str "The type of elimination clause is not well-formed.") in
+    match List.remove Int.equal indmv (clenv_independent elimclause) with
+    | [a] -> a
+    | _ -> user_err ~hdr:"elimination_clause"
+             (str "The type of elimination clause is not well-formed.")
+  in
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
   let hyp_typ = Retyping.get_type_of env sigma hyp in