diff options
-rw-r--r-- | plugins/cc/cctac.ml | 7 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 6 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 3 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 6 | ||||
-rw-r--r-- | plugins/ltac/evar_tactics.ml | 4 | ||||
-rw-r--r-- | plugins/ltac/rewrite.ml | 7 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 6 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml | 17 | ||||
-rw-r--r-- | pretyping/coercion.ml | 8 | ||||
-rw-r--r-- | pretyping/typing.mli | 4 | ||||
-rw-r--r-- | proofs/refine.ml | 23 | ||||
-rw-r--r-- | tactics/tactics.ml | 16 | ||||
-rw-r--r-- | vernac/comFixpoint.ml | 4 | ||||
-rw-r--r-- | vernac/comProgramFixpoint.ml | 4 |
15 files changed, 58 insertions, 60 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c4db49cd3..361981c5b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -49,7 +49,7 @@ let whd_delta env sigma t = (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = e_sort_of env (ref sigma) c +let sf_of env sigma c = snd (sort_of env sigma c) let rec decompose_term env sigma t= match EConstr.kind sigma (whd env sigma t) with @@ -264,9 +264,8 @@ let app_global_with_holes f args n = let ans = mkApp (fc, args) in let (sigma, holes) = gen_holes env sigma t n [] in let ans = applist (ans, holes) in - let evdref = ref sigma in - let () = Typing.e_check env evdref ans concl in - (!evdref, ans) + let sigma = Typing.check env sigma ans concl in + (sigma, ans) end end diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index a0616b308..44fa0740d 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1051,7 +1051,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in evd:=evd'; - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in + evd := sigma; res in let nb_intro_to_do = nb_prod (project g) (pf_concl g) in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 04a23cdb9..dc0f240bd 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -291,7 +291,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in + evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -630,7 +631,8 @@ let build_scheme fas = in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in + evd := sigma; let c, u = try EConstr.destConst !evd f with DestKO -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7df57b577..efbd029e4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -385,7 +385,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in - let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in + let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in + evd := sigma; let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 28e85268a..094f54156 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -103,7 +103,8 @@ let generate_type evd g_to_f f graph i = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) in evd:=evd'; - let graph_arity = Typing.e_type_of (Global.env ()) evd graph in + let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in + evd := sigma; let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with @@ -769,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in + let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in + evd := sigma; let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 9382f567b..fb6be430f 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -85,9 +85,7 @@ let let_evar name typ = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let sigma = ref sigma in - let _ = Typing.e_sort_of env sigma typ in - let sigma = !sigma in + let sigma, _ = Typing.sort_of env sigma typ in let id = match name with | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9eb55aa5e..1b86583da 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -104,9 +104,8 @@ let extends_undefined evars evars' = let app_poly_check env evars f args = let (evars, cstrs), fc = f evars in - let evdref = ref evars in - let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in - (!evdref, cstrs), t + let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in + (evars, cstrs), t let app_poly_nocheck env evars f args = let evars, fc = f evars in @@ -1469,8 +1468,8 @@ exception RewriteFailure of Pp.t type result = (evar_map * constr option * types) option option let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = + let sigma, sort = Typing.sort_of env sigma concl in let evdref = ref sigma in - let sort = Typing.e_sort_of env evdref concl in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 84049d4ed..a93cf5ae7 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -691,11 +691,9 @@ let interp_may_eval f ist env sigma = function let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let ctxt = EConstr.Unsafe.to_constr ctxt in - let evdref = ref sigma in - let ic = EConstr.Unsafe.to_constr ic in + let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in - !evdref , c + Typing.solve_evars env sigma (EConstr.of_constr c) with | Not_found -> user_err ?loc ~hdr:"interp_may_eval" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b2ac3b5a4..074fcb92e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -505,10 +505,12 @@ let ring_equality env evd (r,add,mul,opp,req) = let op_morph = match opp with Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] - | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let setoid = Typing.e_solve_evars env evd setoid in - let op_morph = Typing.e_solve_evars env evd op_morph in - (setoid,op_morph) + | None -> plapp evd coq_eq_smorph [|r;add;mul|] in + let sigma = !evd in + let sigma, setoid = Typing.solve_evars env sigma setoid in + let sigma, op_morph = Typing.solve_evars env sigma op_morph in + evd := sigma; + (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) evd r req in let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in @@ -595,7 +597,8 @@ let make_hyp_list env evdref lH = (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH (plapp evdref coq_nil [|carrier|]) in - let l' = Typing.e_solve_evars env evdref l in + let sigma, l' = Typing.solve_evars env !evdref l in + evdref := sigma; let l' = EConstr.Unsafe.to_constr l' in Evarutil.nf_evars_universes !evdref l' @@ -733,7 +736,9 @@ let make_term_list env evd carrier rl = let l = List.fold_right (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl (plapp evd coq_nil [|carrier|]) - in Typing.e_solve_evars env evd l + in + let sigma, l = Typing.solve_evars env !evd l in + evd := sigma; l let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c) let tacarg expr = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index ea8557b18..c9c2445a7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -197,7 +197,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - Typing.e_solve_evars env evdref term) + let sigma, term = Typing.solve_evars env !evdref term in + evdref := sigma; term) in if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) @@ -343,8 +344,9 @@ let app_coercion env evdref coercion v = match coercion with | None -> v | Some f -> - let v' = Typing.e_solve_evars env evdref (f v) in - whd_betaiota !evdref v' + let sigma, v' = Typing.solve_evars env !evdref (f v) in + evdref := sigma; + whd_betaiota !evdref v' let coerce_itf ?loc env evd v t c1 = let evdref = ref evd in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index da05102f2..3cf43ace0 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -26,14 +26,17 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Variant of [type_of] using references instead of state-passing. *) val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types +[@@ocaml.deprecated "Use [Typing.type_of]"] (** Typecheck a type and return its sort *) val sort_of : env -> evar_map -> types -> evar_map * Sorts.t val e_sort_of : env -> evar_map ref -> types -> Sorts.t +[@@ocaml.deprecated "Use [Typing.sort_of]"] (** Typecheck a term has a given type (assuming the type is OK) *) val check : env -> evar_map -> constr -> types -> evar_map val e_check : env -> evar_map ref -> constr -> types -> unit +[@@ocaml.deprecated "Use [Typing.check]"] (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types @@ -41,6 +44,7 @@ val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) val solve_evars : env -> evar_map -> constr -> evar_map * constr val e_solve_evars : env -> evar_map ref -> constr -> constr +[@@ocaml.deprecated "Use [Typing.solve_evars]"] (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) diff --git a/proofs/refine.ml b/proofs/refine.ml index 5a2d82977..b64e7a2e5 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -30,26 +30,19 @@ let typecheck_evar ev env sigma = (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = let t = NamedDecl.get_type decl in - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref t in - let () = match decl with - | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref body t + let sigma, _ = Typing.sort_of env sigma t in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,body,_) -> Typing.check env sigma body t in - (!evdref, EConstr.push_named decl env) + (sigma, EConstr.push_named decl env) in let (common, changed) = extract_prefix env info in let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in - !evdref - -let typecheck_proof c concl env sigma = - let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in - !evdref + let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in + sigma let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () @@ -93,7 +86,7 @@ let generic_refine ~typecheck f gl = let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) - let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in + let sigma = if typecheck then Typing.check env sigma c concl else sigma in (** Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 60070e6fe..01351e249 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1985,24 +1985,22 @@ let on_the_bodies = function exception DependsOnBody of Id.t option let check_is_type env sigma ty = - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - !evdref + let sigma, _ = Typing.sort_of env sigma ty in + sigma with e when CErrors.noncritical e -> raise (DependsOnBody None) let check_decl env sigma decl = let open Context.Named.Declaration in let ty = NamedDecl.get_type decl in - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - let _ = match decl with - | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.e_check env evdref c ty + let sigma, _ = Typing.sort_of env sigma ty in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,c,_) -> Typing.check env sigma c ty in - !evdref + sigma with e when CErrors.noncritical e -> let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 7b382dacc..85c0699ea 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -199,9 +199,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = try let sigma, h_term = fix_proto sigma in let app = mkApp (h_term, [|sort; t|]) in - let _evd = ref sigma in - let res = Typing.e_solve_evars env _evd app in - !_evd, res + Typing.solve_evars env sigma app with e when CErrors.noncritical e -> sigma, t in sigma, LocalAssum (id,fixprot) :: env' diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 745f1df1d..349fc562b 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -190,9 +190,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in - let _evd = ref sigma in - let def = Typing.e_solve_evars env _evd def in - let sigma = !_evd in + let sigma, def = Typing.solve_evars env sigma def in let sigma = Evarutil.nf_evar_map sigma in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context sigma binders_rel in |