From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- proofs/logic.ml | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) (limited to 'proofs/logic.ml') 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 -- cgit v1.2.3