aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-06 17:21:44 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:25:30 +0100
commite27949240f5b1ee212e7d0fe3326a21a13c4abb0 (patch)
treebf076ea31e6ca36cc80e0f978bc63d112e183725
parentb365304d32db443194b7eaadda63c784814f53f1 (diff)
Typing API using EConstr.
-rw-r--r--ltac/evar_tactics.ml2
-rw-r--r--ltac/rewrite.ml18
-rw-r--r--ltac/tacinterp.ml4
-rw-r--r--plugins/cc/cctac.ml10
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml4
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml10
-rw-r--r--plugins/funind/functional_principles_types.ml10
-rw-r--r--plugins/funind/glob_term_to_relation.ml18
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/setoid_ring/newring.ml8
-rw-r--r--pretyping/cases.ml10
-rw-r--r--pretyping/coercion.ml12
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/typing.ml80
-rw-r--r--pretyping/typing.mli16
-rw-r--r--pretyping/unification.ml4
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/logic.ml4
-rw-r--r--proofs/refine.ml8
-rw-r--r--proofs/tacmach.ml8
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/equality.ml16
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/tactics.ml26
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/command.ml8
31 files changed, 169 insertions, 147 deletions
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index c5b26e6d5..5d3b2b886 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -77,7 +77,7 @@ let let_evar name typ =
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 _ = Typing.e_sort_of env sigma (EConstr.of_constr typ) in
let sigma = Sigma.Unsafe.of_evar_map !sigma in
let id = match name with
| Names.Anonymous ->
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 076e4c05e..5703687c4 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -113,7 +113,7 @@ 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
+ let t = Typing.e_solve_evars env evdref (EConstr.of_constr (mkApp (fc, args))) in
(!evdref, cstrs), t
let app_poly_nocheck env evars f args =
@@ -382,7 +382,7 @@ end
let type_app_poly env env evd f args =
let evars, c = app_poly_nocheck env evd f args in
- let evd', t = Typing.type_of env (goalevars evars) c in
+ let evd', t = Typing.type_of env (goalevars evars) (EConstr.of_constr c) in
(evd', cstrevars evars), c
module PropGlobal = struct
@@ -485,7 +485,7 @@ let rec decompose_app_rel env evd t =
| App (f, [||]) -> assert false
| App (f, [|arg|]) ->
let (f', argl, argr) = decompose_app_rel env evd arg in
- let ty = Typing.unsafe_type_of env evd argl in
+ let ty = Typing.unsafe_type_of env evd (EConstr.of_constr argl) in
let f'' = mkLambda (Name default_dependent_ident, ty,
mkLambda (Name (Id.of_string "y"), lift 1 ty,
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
@@ -787,7 +787,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let morphargs, morphobjs = Array.chop first args in
let morphargs', morphobjs' = Array.chop first args' in
let appm = mkApp(m, morphargs) in
- let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
+ let appmtype = Typing.unsafe_type_of env (goalevars evars) (EConstr.of_constr appm) in
let cstrs = List.map
(Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
(Array.to_list morphobjs')
@@ -1477,7 +1477,7 @@ 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 evdref = ref sigma in
- let sort = Typing.e_sort_of env evdref concl in
+ let sort = Typing.e_sort_of env evdref (EConstr.of_constr concl) in
let evars = (!evdref, Evar.Set.empty) in
let evars, cstr =
let prop, (evars, arrow) =
@@ -1870,7 +1870,7 @@ let declare_projection n instance_id r =
let sigma,c = Evd.fresh_global env sigma r in
let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let term = proper_projection c ty in
- let sigma, typ = Typing.type_of env sigma term in
+ let sigma, typ = Typing.type_of env sigma (EConstr.of_constr term) in
let ctx, typ = decompose_prod_assum typ in
let typ =
let n =
@@ -1902,7 +1902,7 @@ let declare_projection n instance_id r =
let build_morphism_signature env sigma m =
let m,ctx = Constrintern.interp_constr env sigma m in
let sigma = Evd.from_ctx ctx in
- let t = Typing.unsafe_type_of env sigma m in
+ let t = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in
let cstrs =
let rec aux t =
match kind_of_term t with
@@ -1932,7 +1932,7 @@ let build_morphism_signature env sigma m =
let default_morphism sign m =
let env = Global.env () in
let sigma = Evd.from_env env in
- let t = Typing.unsafe_type_of env sigma m in
+ let t = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in
let evars, _, sign, cstrs =
PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
@@ -2126,7 +2126,7 @@ let setoid_proof ty fn fallback =
begin
try
let rel, _, _ = decompose_app_rel env sigma concl in
- let (sigma, t) = Typing.type_of env sigma rel in
+ let (sigma, t) = Typing.type_of env sigma (EConstr.of_constr rel) in
let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in
(try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 34faa028f..8f5ac7e76 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -791,7 +791,7 @@ let interp_may_eval f ist env sigma = function
let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
let evdref = ref sigma in
let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
- let c = Typing.e_solve_evars env evdref c in
+ let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
!evdref , c
with
| Not_found ->
@@ -799,7 +799,7 @@ let interp_may_eval f ist env sigma = function
(str "Unbound context identifier" ++ pr_id s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
- Typing.type_of ~refresh:true env sigma c_interp
+ Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp)
| ConstrTerm c ->
try
f ist env sigma c
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 36a96fdb5..58454eedf 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -50,7 +50,7 @@ let whd_delta env=
(* 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 = e_sort_of env (ref sigma) (EConstr.of_constr c)
let rec decompose_term env sigma t=
match kind_of_term (whd env t) with
@@ -247,7 +247,7 @@ let new_refine c = Proofview.V82.tactic (refine c)
let assert_before n c =
Proofview.Goal.enter { enter = begin fun gl ->
- let evm, _ = Tacmach.New.pf_apply type_of gl c in
+ let evm, _ = Tacmach.New.pf_apply type_of gl (EConstr.of_constr c) in
Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
end }
@@ -340,7 +340,7 @@ let refute_tac c t1 t2 p =
end }
let refine_exact_check c gl =
- let evm, _ = pf_apply type_of gl c in
+ let evm, _ = pf_apply type_of gl (EConstr.of_constr c) in
Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
let convert_to_goal_tac c t1 t2 p =
@@ -480,10 +480,10 @@ let mk_eq f c1 c2 k =
Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
Proofview.Goal.enter { enter = begin fun gl ->
let open Tacmach.New in
- let evm, ty = pf_apply type_of gl c1 in
+ let evm, ty = pf_apply type_of gl (EConstr.of_constr c1) in
let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in
let term = mkApp (fc, [| ty; c1; c2 |]) in
- let evm, _ = type_of (pf_env gl) evm term in
+ let evm, _ = type_of (pf_env gl) evm (EConstr.of_constr term) in
Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
(k term)
end })
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index c17c8dbb8..dcebf7806 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -429,7 +429,7 @@ let concl_refiner metas body gls =
let concl = pf_concl gls in
let evd = sig_sig gls in
let env = pf_env gls in
- let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
+ let sort = family_of_sort (Typing.e_sort_of env (ref evd) (EConstr.of_constr concl)) in
let rec aux env avoid subst = function
[] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
| (n,typ)::rest ->
@@ -437,7 +437,7 @@ let concl_refiner metas body gls =
let x = id_of_name_using_hdchar env _A Anonymous in
let _x = fresh_id avoid x gls in
let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
- let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
+ let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in
let nsubst = (n,mkVar _x)::subst in
if List.is_empty rest then
asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a3513692c..44bdb585a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -155,7 +155,7 @@ let left_instance_tac (inst,id) continue seq=
it_mkLambda_or_LetIn
(mkApp(idc,[|ot|])) rc in
let evmap, _ =
- try Typing.type_of (pf_env gl) evmap gt
+ try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt)
with e when CErrors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 340dd2c28..0a7938069 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -329,7 +329,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
let all_ids = pf_ids_of_hyps g in
let new_ids,_ = list_chop ctxt_size all_ids in
let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
- let evm, _ = pf_apply Typing.type_of g to_refine in
+ let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr to_refine) in
tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
)
in
@@ -544,7 +544,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
tclIDTAC
in
try
- scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
+ scan_type [] (Typing.unsafe_type_of env sigma (EConstr.mkVar hyp_id)), [hyp_id]
with TOREMOVE ->
thin [hyp_id],[]
@@ -639,7 +639,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
fun g ->
let prov_hid = pf_get_new_id hid g in
let c = mkApp(mkVar hid,args) in
- let evm, _ = pf_apply Typing.type_of g c in
+ let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr c) in
tclTHENLIST[
Refiner.tclEVARS evm;
Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -968,7 +968,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
(* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *)
let (type_ctxt,type_of_f),evd =
- let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
+ let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f)
in
decompose_prod_n_assum
(nb_params + nb_args) t,evd
@@ -1039,7 +1039,7 @@ 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 _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr res) in
res
in
let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9637632a6..4b47b83af 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -283,7 +283,7 @@ 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_________") []
in
- let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in
+ let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
let hook = Lemmas.mk_hook (hook new_principle_type) in
begin
Lemmas.start_proof
@@ -337,7 +337,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
- let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
+ let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
ignore(
@@ -488,7 +488,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
in
let _ = evd := sigma in
let l_schemes =
- List.map (Typing.unsafe_type_of env sigma) schemes
+ List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma) schemes
in
let i = ref (-1) in
let sorts =
@@ -616,7 +616,7 @@ 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 _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in
(destConst f,sort)
)
fas
@@ -666,7 +666,7 @@ let build_case_scheme fa =
Indrec.build_case_analysis_scheme_default env sigma ind sf
in
let sigma = Sigma.to_evar_map sigma in
- let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in
+ let scheme_type = (Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme) in
let sorts =
(fun (_,_,x) ->
Universes.new_sort_in_family (Pretyping.interp_elimination_sort x)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 92de4d873..38cd21684 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -503,7 +503,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
The "value" of this branch is then simply [res]
*)
let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
- let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+ let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
let new_avoid = res::args_res.to_avoid in
@@ -611,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
let v_res = build_entry_lc env funnames avoid v in
let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
- let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
+ let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
let new_env =
match n with
Anonymous -> env
@@ -627,7 +627,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
build_entry_lc_from_case env funnames make_discr el brl avoid
| GIf(_,b,(na,e_option),lhs,rhs) ->
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
- let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
with Not_found ->
@@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
nal
in
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
- let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+ let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
with Not_found ->
@@ -706,7 +706,7 @@ and build_entry_lc_from_case env funname make_discr
let types =
List.map (fun (case_arg,_) ->
let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
- Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr
+ Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr)
) el
in
(****** The next works only if the match is not dependent ****)
@@ -753,7 +753,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
List.fold_right
(fun id acc ->
let typ_of_id =
- Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id)
+ Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
in
let raw_typ_of_id =
Detyping.detype false []
@@ -807,7 +807,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
(fun id acc ->
if Id.Set.mem id this_pat_ids
then (Prod (Name id),
- let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in
+ let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
let raw_typ_of_id =
Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
in
@@ -1121,7 +1121,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let evd = (Evd.from_env env) in
let t',ctx = Pretyping.understand env evd t in
let evd = Evd.from_ctx ctx in
- let type_t' = Typing.unsafe_type_of env evd t' in
+ let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in
let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in
let new_b,id_to_exclude =
rebuild_cons new_env
@@ -1272,7 +1272,7 @@ let do_build_inductive
let evd,env =
Array.fold_right2
(fun id c (evd,env) ->
- let evd,t = Typing.type_of env evd (mkConstU c) in
+ let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in
evd,
Environ.push_named (LocalAssum (id,t))
(* try *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a264c37c5..0743fc5d9 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -369,7 +369,7 @@ 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 princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in
Functional_principles_types.generate_functional_principle
evd
interactive_proof
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9abe60402..e5286fb1f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -134,7 +134,7 @@ let generate_type evd g_to_f f graph i =
Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd graph)))
in
evd:=evd';
- let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+ let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
let ctxt,_ = decompose_prod_assum graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -202,7 +202,7 @@ let find_induction_principle evd f =
| None -> raise Not_found
| Some rect_lemma ->
let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in
- let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+ let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
evd:=evd';
rect_lemma,typ
@@ -449,7 +449,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
"functional_induction" (
(fun gl ->
let term = mkApp (mkVar principle_id,Array.of_list bindings) in
- let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl term in
+ let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl (EConstr.of_constr term) in
Proofview.V82.of_tactic (apply term) gl')
))
(fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -792,7 +792,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
let type_of_lemma = Termops.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 _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in
let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
type_of_lemma,type_info
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4fd9e0ff8..12ed758ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -657,7 +657,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden}
let pf_type c tac gl =
- let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
+ let evars, ty = Typing.type_of (pf_env gl) (project gl) (EConstr.of_constr c) in
tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
let pf_typel l tac =
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e1b95ddbc..b0a3e839b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -493,8 +493,8 @@ let ring_equality env evd (r,add,mul,opp,req) =
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
+ let setoid = Typing.e_solve_evars env evd (EConstr.of_constr setoid) in
+ let op_morph = Typing.e_solve_evars env evd (EConstr.of_constr op_morph) in
(setoid,op_morph)
| _ ->
let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -581,7 +581,7 @@ let make_hyp_list env evd lH =
(fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
(plapp evd coq_nil [|carrier|])
in
- let l' = Typing.e_solve_evars env evd l in
+ let l' = Typing.e_solve_evars env evd (EConstr.of_constr l) in
Evarutil.nf_evars_universes !evd l'
let interp_power env evd pow =
@@ -707,7 +707,7 @@ 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 Typing.e_solve_evars env evd (EConstr.of_constr l)
let carg = Tacinterp.Value.of_constr
let tacarg expr =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 04f50d50e..882c052f6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1381,7 +1381,7 @@ and match_current pb (initial,tomatch) =
let case =
make_case_or_project pb.env indf ci pred current brvals
in
- Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
+ Typing.check_allowed_sort pb.env !(pb.evdref) mind (EConstr.of_constr current) (EConstr.of_constr pred);
{ uj_val = applist (case, inst);
uj_type = prod_applist typ inst }
@@ -1684,7 +1684,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
(lift (n'-n) impossible_case_type, mkSort u)
| Some t ->
let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
- let evd,tt = Typing.type_of extenv !evdref t in
+ let evd,tt = Typing.type_of extenv !evdref (EConstr.of_constr t) in
evdref := evd;
(t,tt) in
let b = e_cumul env evdref (EConstr.of_constr tt) (EConstr.mkSort s) (* side effect *) in
@@ -1920,7 +1920,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
assert (len == 0);
let p = predicate 0 c in
let env' = List.fold_right push_rel_context arsign env in
- try let sigma' = fst (Typing.type_of env' sigma p) in
+ try let sigma' = fst (Typing.type_of env' sigma (EConstr.of_constr p)) in
Some (sigma', p)
with e when precatchable_exception e -> None
@@ -2041,7 +2041,7 @@ let constr_of_pat env evdref arsign pat avoid =
let IndType (indf, _) =
try find_rectype env ( !evdref) (EConstr.of_constr (lift (-(List.length realargs)) ty))
with Not_found -> error_case_not_inductive env !evdref
- {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
+ {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref (EConstr.of_constr ty)}
in
let (ind,u), params = dest_ind_family indf in
if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind;
@@ -2242,7 +2242,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
let j = typing_fun (mk_tycon (EConstr.of_constr tycon)) rhs_env eqn.rhs.it in
let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
- let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
+ let _btype = evd_comb1 (Typing.type_of env) evdref (EConstr.of_constr bbody) in
let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
let branch =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0ea6758a7..04e235cc5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -188,7 +188,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
aux (hdy :: tele) (subst1 hdx restT)
(subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some (fun x ->
- let term = co x in
+ let term = EConstr.of_constr (co x) in
Typing.e_solve_evars env evdref term)
in
if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
@@ -297,16 +297,16 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let evm = !evdref in
(try subco ()
with NoSubtacCoercion ->
- let typ = Typing.unsafe_type_of env evm c in
- let typ' = Typing.unsafe_type_of env evm c' in
+ let typ = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
+ let typ' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
coerce_application typ typ' c c' l l')
else
subco ()
| x, y when Constr.equal c c' ->
if Int.equal (Array.length l) (Array.length l') then
let evm = !evdref in
- let lam_type = Typing.unsafe_type_of env evm c in
- let lam_type' = Typing.unsafe_type_of env evm c' in
+ let lam_type = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
+ let lam_type' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
coerce_application lam_type lam_type' c c' l l'
else subco ()
| _ -> subco ())
@@ -337,7 +337,7 @@ 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
+ let v' = Typing.e_solve_evars env evdref (EConstr.of_constr (f v)) in
whd_betaiota !evdref (EConstr.of_constr v')
let coerce_itf loc env evd v t c1 =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 570f95324..28ba60812 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -507,7 +507,7 @@ let pretype_ref loc evdref env ref us =
| ref ->
let evd, c = pretype_global loc univ_flexible env !evdref ref us in
let () = evdref := evd in
- let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in
+ let ty = Typing.unsafe_type_of env.ExtraEnv.env evd (EConstr.of_constr c) in
make_judge c ty
let judge_of_Type loc evd s =
@@ -644,7 +644,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
- Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj;
+ Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names (Array.map EConstr.of_constr ftys) vdefj;
let ftys = Array.map (nf_evar !evdref) ftys in
let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
let fixj = match fixkind with
@@ -898,7 +898,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in
let v =
let ind,_ = dest_ind_family indf in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+ Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p);
obj ind p cj.uj_val fj.uj_val
in
{ uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
@@ -917,7 +917,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
let ind,_ = dest_ind_family indf in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+ Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p);
obj ind p cj.uj_val fj.uj_val
in { uj_val = v; uj_type = ccl })
@@ -981,7 +981,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let ind,_ = dest_ind_family indf in
let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
let pred = nf_evar !evdref pred in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
+ Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr pred);
mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
let cj = { uj_val = v; uj_type = p } in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 290d77b1b..a3983737d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1164,7 +1164,7 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
let sigma = Sigma.to_evar_map sigma in
let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (EConstr.Unsafe.to_constr c,sigma) in
try
- let _ = Typing.unsafe_type_of env sigma abstr_trm in
+ let _ = Typing.unsafe_type_of env sigma (EConstr.of_constr abstr_trm) in
Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
with Type_errors.TypeError (env',t) ->
raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 64264cf08..c948f9b9a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -20,6 +20,11 @@ open Typeops
open Arguments_renaming
open Context.Rel.Declaration
+let push_rec_types pfix env =
+ let (i, c, t) = pfix in
+ let inj c = EConstr.Unsafe.to_constr c in
+ push_rec_types (i, Array.map inj c, Array.map inj t) env
+
let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
@@ -28,12 +33,12 @@ let meta_type evd mv =
let constant_type_knowing_parameters env cst jl =
let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
- type_of_constant_knowing_parameters_in env cst paramstyp
+ EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
let inductive_type_knowing_parameters env (ind,u) jl =
let mspec = lookup_mind_specif env ind in
let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
- Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+ EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
let e_type_judgment env evdref j =
match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
@@ -44,7 +49,7 @@ let e_type_judgment env evdref j =
| _ -> error_not_type env j
let e_assumption_of_judgment env evdref j =
- try (e_type_judgment env evdref j).utj_val
+ try EConstr.of_constr (e_type_judgment env evdref j).utj_val
with TypeError _ ->
error_assumption env j
@@ -84,27 +89,28 @@ let max_sort l =
if Sorts.List.mem InSet l then InSet else InProp
let e_is_correct_arity env evdref c pj ind specif params =
+ let open EConstr in
let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
let allowed_sorts = elim_sorts specif in
let error () = error_elim_arity env ind allowed_sorts c pj None in
let rec srec env pt ar =
- let pt' = whd_all env !evdref (EConstr.of_constr pt) in
- match kind_of_term pt', ar with
+ let pt' = EConstr.of_constr (whd_all env !evdref pt) in
+ match EConstr.kind !evdref pt', ar with
| Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
- if not (Evarconv.e_cumul env evdref (EConstr.of_constr a1) (EConstr.of_constr a1')) then error ();
- srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+ if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
+ srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar'
| Sort s, [] ->
if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
then error ()
| Evar (ev,_), [] ->
let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
- evdref := Evd.define ev (mkSort s) evd
+ evdref := Evd.define ev (Constr.mkSort s) evd
| _, (LocalDef _ as d)::ar' ->
- srec (push_rel d env) (lift 1 pt') ar'
+ srec (push_rel d env) (Vars.lift 1 pt') ar'
| _ ->
error ()
in
- srec env pj.uj_type (List.rev arsign)
+ srec env (EConstr.of_constr pj.uj_type) (List.rev arsign)
let e_type_case_branches env evdref (ind,largs) pj c =
let specif = lookup_mind_specif env (fst ind) in
@@ -128,24 +134,25 @@ let e_judge_of_case env evdref ci pj cj lfj =
uj_type = rslty }
let check_type_fixpoint loc env evdref lna lar vdefj =
+ let open EConstr in
let lt = Array.length vdefj in
if Int.equal (Array.length lar) lt then
for i = 0 to lt-1 do
if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
- (EConstr.of_constr (lift lt lar.(i)))) then
+ (Vars.lift lt lar.(i))) then
Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
- i lna vdefj lar
+ i lna vdefj (Array.map EConstr.Unsafe.to_constr lar)
done
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
- let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in
+ let pj = Retyping.get_judgment_of env sigma p in
let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
let specif = Global.lookup_inductive (fst ind) in
let sorts = elim_sorts specif in
if not (List.exists ((==) ksort) sorts) then
let s = inductive_sort_family (snd specif) in
- error_elim_arity env ind sorts c pj
+ error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj
(Some(ksort,s,error_elim_explain ksort s))
let e_judge_of_cast env evdref cj k tj =
@@ -160,21 +167,36 @@ let enrich_env env evdref =
let penv' = Pre_env.({ penv with env_stratification =
{ penv.env_stratification with env_universes = Evd.universes !evdref } }) in
Environ.env_of_pre_env penv'
+
+let check_fix env sigma pfix =
+ let inj c = EConstr.to_constr sigma c in
+ let (idx, (ids, cs, ts)) = pfix in
+ check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let check_cofix env sigma pcofix =
+ let inj c = EConstr.to_constr sigma c in
+ let (idx, (ids, cs, ts)) = pcofix in
+ check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let make_judge c ty =
+ make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
(* The typing machine with universes and existential variables. *)
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
let rec execute env evdref cstr =
- match kind_of_term cstr with
+ let open EConstr in
+ let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
+ match EConstr.kind !evdref cstr with
| Meta n ->
- { uj_val = cstr; uj_type = meta_type !evdref n }
+ { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n }
| Evar ev ->
- let ty = Evd.existential_type !evdref ev in
- let jty = execute env evdref (whd_evar !evdref ty) in
+ let ty = EConstr.existential_type !evdref ev in
+ let jty = execute env evdref ty in
let jty = e_assumption_of_judgment env evdref jty in
- { uj_val = cstr; uj_type = jty }
+ { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty }
| Rel n ->
judge_of_relative env n
@@ -183,13 +205,13 @@ let rec execute env evdref cstr =
judge_of_variable env id
| Const c ->
- make_judge cstr (rename_type_of_constant env c)
+ make_judge cstr (EConstr.of_constr (rename_type_of_constant env c))
| Ind ind ->
- make_judge cstr (rename_type_of_inductive env ind)
+ make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind))
| Construct cstruct ->
- make_judge cstr (rename_type_of_constructor env cstruct)
+ make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct))
| Case (ci,p,c,lf) ->
let cj = execute env evdref c in
@@ -200,13 +222,13 @@ let rec execute env evdref cstr =
| Fix ((vn,i as vni),recdef) ->
let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
let fix = (vni,recdef') in
- check_fix env fix;
+ check_fix env !evdref fix;
make_judge (mkFix fix) tys.(i)
| CoFix (i,recdef) ->
let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
let cofix = (i,recdef') in
- check_cofix env cofix;
+ check_cofix env !evdref cofix;
make_judge (mkCoFix cofix) tys.(i)
| Sort (Prop c) ->
@@ -222,7 +244,7 @@ let rec execute env evdref cstr =
| App (f,args) ->
let jl = execute_array env evdref args in
let j =
- match kind_of_term f with
+ match EConstr.kind !evdref f with
| Ind ind when Environ.template_polymorphic_pind ind env ->
(* Sort-polymorphism of inductive types *)
make_judge f
@@ -273,7 +295,7 @@ and execute_recdef env evdref (names,lar,vdef) =
let lara = Array.map (e_assumption_of_judgment env evdref) larj in
let env1 = push_rec_types (names,lara,vdef) env in
let vdefj = execute_array env1 evdref vdef in
- let vdefv = Array.map j_val vdefj in
+ let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in
let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
(names,lara,vdefv)
@@ -282,8 +304,8 @@ and execute_array env evdref = Array.map (execute env evdref)
let e_check env evdref c t =
let env = enrich_env env evdref in
let j = execute env evdref c in
- if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) (EConstr.of_constr t)) then
- error_actual_type env j (nf_evar !evdref t)
+ if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then
+ error_actual_type env j (EConstr.to_constr !evdref t)
(* Type of a constr *)
@@ -328,4 +350,4 @@ let e_solve_evars env evdref c =
(* side-effect on evdref *)
nf_evar !evdref c
-let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref (EConstr.Unsafe.to_constr c)))
+let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 04e5e40bc..3c1c4324d 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -14,33 +14,33 @@ open Evd
and universes. *)
(** Typecheck a term and return its type. May trigger an evarmap leak. *)
-val unsafe_type_of : env -> evar_map -> constr -> types
+val unsafe_type_of : env -> evar_map -> EConstr.constr -> types
(** Typecheck a term and return its type + updated evars, optionally refreshing
universes *)
-val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+val type_of : ?refresh:bool -> env -> evar_map -> EConstr.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
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> types
(** Typecheck a type and return its sort *)
-val e_sort_of : env -> evar_map ref -> types -> sorts
+val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts
(** Typecheck a term has a given type (assuming the type is OK) *)
-val e_check : env -> evar_map ref -> constr -> types -> unit
+val e_check : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit
(** Returns the instantiated type of a metavariable *)
val meta_type : evar_map -> metavariable -> types
(** Solve existential variables using typing *)
-val e_solve_evars : env -> evar_map ref -> constr -> constr
+val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr
(** Raise an error message if incorrect elimination for this inductive *)
(** (first constr is term to match, second is return predicate) *)
-val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
+val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.constr ->
unit
(** Raise an error message if bodies have types not unifiable with the
expected ones *)
val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
- Names.Name.t array -> types array -> unsafe_judgment array -> unit
+ Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ac2f14051..f418dc6a9 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -102,7 +102,7 @@ let abstract_list_all env evd typ c l =
let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
let evd,typp =
- try Typing.type_of env evd p
+ try Typing.type_of env evd (EConstr.of_constr p)
with
| UserError _ ->
error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) None
@@ -1214,7 +1214,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
| _ -> error "Apply_Head_Then"
in
- apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
+ apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) (EConstr.of_constr c)) Sigma.refl evd
let is_mimick_head ts f =
match kind_of_term f with
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f4ac094b8..c2130a64a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -29,7 +29,7 @@ open Sigma.Notations
(* Abbreviations *)
let pf_env = Refiner.pf_env
-let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c
+let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c)
(******************************************************************)
(* Clausal environments *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2df626e1c..93b31ced1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -86,7 +86,7 @@ let apply_to_hyp check sign id f =
else sign
let check_typability env sigma c =
- if !check then let _ = unsafe_type_of env sigma c in ()
+ if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
(************************************************************************)
(************************************************************************)
@@ -330,7 +330,7 @@ let meta_free_prefix sigma a =
with Stop acc -> Array.rev_of_list acc
let goal_type_of env sigma c =
- if !check then unsafe_type_of env sigma c
+ if !check then unsafe_type_of env sigma (EConstr.of_constr c)
else Retyping.get_type_of env sigma (EConstr.of_constr c)
let rec mk_refgoals sigma goal goalacc conclty trm =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index e6e3ef47d..b62f0bea4 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -28,12 +28,12 @@ let typecheck_evar ev env sigma =
let info = Evd.find sigma ev in
(** Typecheck the hypotheses. *)
let type_hyp (sigma, env) decl =
- let t = NamedDecl.get_type decl in
+ let t = EConstr.of_constr (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
+ | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
in
(!evdref, Environ.push_named decl env)
in
@@ -42,12 +42,12 @@ let typecheck_evar ev env sigma =
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
+ let _ = Typing.e_sort_of env evdref (EConstr.of_constr (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
+ let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in
!evdref
let (pr_constrv,pr_constr) =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b63b2ce28..148f9d675 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -93,8 +93,8 @@ let pf_nf = pf_reduce' simpl
let pf_nf_betaiota = pf_reduce' (fun _ -> nf_betaiota)
let pf_compute = pf_reduce' compute
let pf_unfoldn ubinds = pf_reduce' (unfoldn ubinds)
-let pf_unsafe_type_of = pf_reduce unsafe_type_of
-let pf_type_of = pf_reduce type_of
+let pf_unsafe_type_of = pf_reduce' unsafe_type_of
+let pf_type_of = pf_reduce' type_of
let pf_get_type_of = pf_reduce Retyping.get_type_of
let pf_conv_x gl = pf_apply test_conversion gl Reduction.CONV
@@ -175,10 +175,10 @@ module New = struct
let pf_concl = Proofview.Goal.concl
let pf_unsafe_type_of gl t =
- pf_apply unsafe_type_of gl t
+ pf_apply unsafe_type_of gl (EConstr.of_constr t)
let pf_type_of gl t =
- pf_apply type_of gl t
+ pf_apply type_of gl (EConstr.of_constr t)
let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 46600cdd7..80b9ec06e 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -272,7 +272,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
try
let others,(c1,c2) = split_last_two args in
let ty1, ty2 =
- Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2
+ Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2)
in
(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* else *)
@@ -290,7 +290,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
| None -> None
let find_applied_relation metas loc env sigma c left2right =
- let ctype = Typing.unsafe_type_of env sigma c in
+ let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
match decompose_applied_relation metas env sigma c ctype left2right with
| Some c -> c
| None ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 17038e42d..58c86ff42 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1085,7 +1085,7 @@ let find_sigma_data env s = build_sigma_type ()
let make_tuple env sigma (rterm,rty) lind =
assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in
- let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+ let sigma, a = type_of ~refresh:true env sigma (EConstr.mkRel lind) in
let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
(* We move [lind] to [1] and lift other rels > [lind] by 1 *)
let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1119,7 +1119,7 @@ let minimal_free_rels_rec env sigma =
let rec minimalrec_free_rels_rec prev_rels (c,cty) =
let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
let combined_rels = Int.Set.union prev_rels direct_rels in
- let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
+ let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (EConstr.mkRel i)))
in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
in minimalrec_free_rels_rec Int.Set.empty
@@ -1165,7 +1165,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let rec sigrec_clausal_form siglen p_i =
if Int.equal siglen 0 then
(* is the default value typable with the expected type *)
- let dflt_typ = unsafe_type_of env sigma dflt in
+ let dflt_typ = unsafe_type_of env sigma (EConstr.of_constr dflt) in
try
let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
@@ -1184,7 +1184,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
(destEvar ev)
with
| Some w ->
- let w_type = unsafe_type_of env sigma w in
+ let w_type = unsafe_type_of env sigma (EConstr.of_constr w) in
if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
@@ -1273,7 +1273,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
sigma, (tuple,tuplety,dfltval)
let rec build_injrec env sigma dflt c = function
- | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
+ | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma (EConstr.of_constr c))
| ((sp,cnum),argnum)::l ->
try
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1367,7 +1367,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let injfun = mkNamedLambda e t injbody in
let sigma,congr = Evd.fresh_global env sigma eq.congr in
let pf = applist(congr,[t;resty;injfun;t1;t2]) in
- let sigma, pf_typ = Typing.type_of env sigma pf in
+ let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta inj_clause in
let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1555,8 +1555,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
(* Retype to get universes right *)
- let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
- let sigma, _ = Typing.type_of env sigma body in
+ let sigma, expected_goal_ty = Typing.type_of env sigma (EConstr.of_constr expected_goal) in
+ let sigma, _ = Typing.type_of env sigma (EConstr.of_constr body) in
Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
(* Like "replace" but decompose dependent equalities *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2aa434777..63d10573a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -910,7 +910,7 @@ let make_mode ref m =
let make_trivial env sigma poly ?(name=PathAny) r =
let c,ctx = fresh_global_or_constr env sigma poly r in
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
- let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
+ let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
let hd = head_of_constr_reference (head_constr sigma t) in
let ce = mk_clenv_from_env env sigma None (c,t) in
(Some hd, { pri=1;
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 38f75995b..9282af759 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl =
let refl_term = eqdata.Coqlib.refl in
let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
let refl = mkApp (refl_term, [|eqnty; rhs|]) in
- let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
+ let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr refl) in
let args = refl :: args in
build_concl eqns args (succ n) restlist
in
let (newconcl, args) = build_concl [] [] 0 realargs in
let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in
- let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
+ let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr predicate) in
(* OK - this predicate should now be usable by res_elimination_then to
do elimination on the conclusion. *)
predicate, args
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c2163a274..8fb47b994 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -210,7 +210,7 @@ let convert_concl ?(check=true) ty k =
let Sigma ((), sigma, p) =
if check then begin
let sigma = Sigma.to_evar_map sigma in
- ignore (Typing.unsafe_type_of env sigma ty);
+ ignore (Typing.unsafe_type_of env sigma (EConstr.of_constr ty));
let sigma,b = Reductionops.infer_conv env sigma ty conclty in
if not b then error "Not convertible.";
Sigma.Unsafe.of_pair ((), sigma)
@@ -827,7 +827,7 @@ let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c ->
env sigma c in
if !mayneedglobalcheck then
begin
- try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c)
+ try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c))
with e when catchable_exception e ->
error "Replacement would lead to an ill-typed term."
end;
@@ -1228,7 +1228,7 @@ let cut c =
let is_sort =
try
(** Backward compat: ensure that [c] is well-typed. *)
- let typ = Typing.unsafe_type_of env sigma c in
+ let typ = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
let typ = whd_all env sigma (EConstr.of_constr typ) in
match kind_of_term typ with
| Sort _ -> true
@@ -1940,7 +1940,7 @@ let exact_check c =
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let env = Proofview.Goal.env gl in
let sigma = Sigma.to_evar_map sigma in
- let sigma, ct = Typing.type_of env sigma c in
+ let sigma, ct = Typing.type_of env sigma (EConstr.of_constr c) in
let tac =
Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)
in
@@ -2009,20 +2009,20 @@ 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
+ let _ = Typing.e_sort_of env evdref (EConstr.of_constr ty) in
!evdref
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 ty = EConstr.of_constr (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
+ | LocalDef (_,c,_) -> Typing.e_check env evdref (EConstr.of_constr c) ty
in
!evdref
with e when CErrors.noncritical e ->
@@ -2622,7 +2622,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
let refl = applist (refl, [t;mkVar id]) in
let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
let sigma = Sigma.to_evar_map sigma in
- let sigma, _ = Typing.type_of env sigma term in
+ let sigma, _ = Typing.type_of env sigma (EConstr.of_constr term) in
let ans = term,
Tacticals.New.tclTHEN
(intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
@@ -2783,7 +2783,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl =
let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
let env = Tacmach.pf_env gl in
let ids = Tacmach.pf_ids_of_hyps gl in
- let sigma, t = Typing.type_of env sigma c in
+ let sigma, t = Typing.type_of env sigma (EConstr.of_constr c) in
generalize_goal_gen env sigma ids i o t cl
let old_generalize_dep ?(with_let=false) c gl =
@@ -2818,7 +2818,7 @@ let old_generalize_dep ?(with_let=false) c gl =
let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
(cl',project gl) in
(** Check that the generalization is indeed well-typed *)
- let (evd, _) = Typing.type_of env evd cl'' in
+ let (evd, _) = Typing.type_of env evd (EConstr.of_constr cl'') in
let args = Context.Named.to_instance to_quantify_rev in
tclTHENLIST
[tclEVARS evd;
@@ -2836,7 +2836,7 @@ let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun
List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
(Tacmach.New.pf_concl gl,Tacmach.New.project gl)
in
- let (evd, _) = Typing.type_of env evd newcl in
+ let (evd, _) = Typing.type_of env evd (EConstr.of_constr newcl) in
let map ((_, c, b),_) = if Option.is_empty b then Some c else None in
let tac = apply_type newcl (List.map_filter map lconstr) in
Sigma.Unsafe.of_pair (tac, evd)
@@ -2853,7 +2853,7 @@ let new_generalize_gen_let lconstr =
let newcl, sigma, args =
List.fold_right_i
(fun i ((_,c,b),_ as o) (cl, sigma, args) ->
- let sigma, t = Typing.type_of env sigma c in
+ let sigma, t = Typing.type_of env sigma (EConstr.of_constr c) in
let args = if Option.is_empty b then c :: args else args in
let cl, sigma = generalize_goal_gen env sigma ids i o t cl in
(cl, sigma, args))
@@ -4738,7 +4738,7 @@ let prove_transitivity hdcncl eq_kind t =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let type_of = Typing.unsafe_type_of env sigma in
- let typt = type_of t in
+ let typt = type_of (EConstr.of_constr t) in
(mkApp(hdcncl, [| typ1; c1; typt ;t |]),
mkApp(hdcncl, [| typt; t; typ2; c2 |]))
in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 5aa000b16..86fd4d9a2 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -206,7 +206,7 @@ let build_id_coercion idf_opt source poly =
let _ =
if not
(Reductionops.is_conv_leq env sigma
- (EConstr.of_constr (Typing.unsafe_type_of env sigma val_f)) (EConstr.of_constr typ_f))
+ (EConstr.of_constr (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f))) (EConstr.of_constr typ_f))
then
user_err (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14a45f837..c6dd3eb99 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -953,7 +953,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let binders = letbinders @ [arg] in
let binders_env = push_rel_context binders_rel env in
let rel, _ = interp_constr_evars_impls env evdref r in
- let relty = Typing.unsafe_type_of env !evdref rel in
+ let relty = Typing.unsafe_type_of env !evdref (EConstr.of_constr rel) in
let relargty =
let error () =
user_err ~loc:(constr_loc r)
@@ -1034,7 +1034,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
prop |])
in
- let def = Typing.e_solve_evars env evdref def in
+ let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in
let _ = evdref := Evarutil.nf_evar_map !evdref in
let def = mkApp (def, [|intern_body_lam|]) in
let binders_rel = nf_evar_context !evdref binders_rel in
@@ -1105,11 +1105,11 @@ let interp_recursive isfix fixl notations =
List.fold_left2
(fun env' id t ->
if Flags.is_program_mode () then
- let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
+ let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref (EConstr.of_constr t) in
let fixprot =
try
let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
- Typing.e_solve_evars env evdref app
+ Typing.e_solve_evars env evdref (EConstr.of_constr app)
with e when CErrors.noncritical e -> t
in
LocalAssum (id,fixprot) :: env'