Imported Upstream version 8.5~beta3+dfsg

1 files changed, 18 insertions, 14 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8206ca1..3273c957 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -83,7 +83,7 @@ let apply_to_hyp sign id f =
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma c in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) =
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    error ("Cannot create self-referring hypothesis "^Id.to_string x);
+    errorlabstrm "Logic.check_decl_position"
+      (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -316,7 +317,7 @@ let meta_free_prefix a =
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then type_of env sigma c
+  if !check then unsafe_type_of env sigma c
   else Retyping.get_type_of env sigma c
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
@@ -355,9 +356,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
 	  if is_template_polymorphic env f then
-	    let sigma, ty = 
+	    let ty = 
 	      (* Template sort-polymorphism of definition and inductive types *)
-	      type_of_global_reference_knowing_conclusion env sigma f conclty
+	      let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
+	        type_of_global_reference_knowing_parameters env sigma f args
 	    in
 	      goalacc, ty, sigma, f
 	  else
@@ -488,9 +491,11 @@ let convert_hyp check sign sigma (id,b,bt as d) =
       (fun _ (_,c,ct) _ ->
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
-	  error ("Incorrect change of the type of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  error ("Incorrect change of the body of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sign d;
        d) in
   reorder_val_context env sign' !reorder
@@ -522,7 +527,8 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      error ("Variable " ^ Id.to_string id ^ " is already declared.");
+	      errorlabstrm "Logic.prim_refiner"
+                (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
@@ -550,11 +556,10 @@ let prim_refiner r sigma goal =
 	  | (f,n,ar)::oth ->
 	      let ((sp',_),u')  = check_ind env n ar in
 	      if not (eq_mind sp sp') then
-		error ("Fixpoints should be on the same " ^
-		       "mutual inductive declaration.");
+		error "Fixpoints should be on the same mutual inductive declaration.";
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error
-		  ("Name "^Id.to_string f^" already used in the environment");
+		errorlabstrm "Logic.prim_refiner"
+		  (str "Name " ++ pr_id f ++ str " already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
 	      Evd.Monad.List.map (fun (_,_,c) sigma ->
@@ -584,8 +589,7 @@ let prim_refiner r sigma goal =
 		try
 		  let _ = find_coinductive env sigma b in ()
                 with Not_found ->
-		  error ("All methods must construct elements " ^
-			  "in coinductive types.")
+		  error "All methods must construct elements in coinductive types."
 	in
 	let firsts,lasts = List.chop j others in
 	let all = firsts@(f,cl)::lasts in