diff options
| author | herbelin | 2005-12-21 15:06:11 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-21 15:06:11 +0000 |
| commit | 2cb47551ded9ccab3c329993ca11cd3c65e84be0 (patch) | |
| tree | 67b682dd63f8445133ab10c9766edca738db9207 /proofs | |
| parent | a36feecff63129e9049cb468ac1b0258442c01a7 (diff) | |
Restructuration des points d'entrée de Pretyping et Constrintern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 6 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
2 files changed, 3 insertions, 7 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 3db11ce390..1591d43c92 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -28,8 +28,8 @@ let w_refine env ev rawc evd = let e_info = Evd.map (evars_of evd) ev in let env = Evd.evar_env e_info in let sigma,typed_c = - Pretyping.understand_gen_tcc (evars_of evd) env [] - (Some e_info.evar_concl) rawc in + Pretyping.understand_tcc (evars_of evd) env + ~expected_type:e_info.evar_concl rawc in evar_define ev typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) @@ -43,7 +43,7 @@ let instantiate_pf_com n com pfts = with Failure _ -> error "not so many uninstantiated existential variables" in let env = Evd.evar_env evi in - let rawc = Constrintern.interp_rawconstr sigma env com in + let rawc = Constrintern.intern_constr sigma env com in let evd = create_evar_defs sigma in let evd' = w_refine env sp rawc evd in change_constraints_pftreestate (evars_of evd') pfts diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7ac7b185b7..adb18daa7a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -79,10 +79,6 @@ let pf_interp_constr gls c = let evc = project gls in Constrintern.interp_constr evc (pf_env gls) c -let pf_interp_openconstr gls c = - let evc = project gls in - Constrintern.interp_openconstr evc (pf_env gls) c - let pf_interp_type gls c = let evc = project gls in Constrintern.interp_type evc (pf_env gls) c |