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 /translate | |
| 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 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 8 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 2 |
2 files changed, 4 insertions, 6 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 5f3cda588a..422b253437 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -670,11 +670,10 @@ let transf istype env iscast bl c = if Options.do_translate() then let r = Constrintern.for_grammar - (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[])) - c' in + (Constrintern.intern_gen istype Evd.empty env) c' in begin try (* Try to infer old case and type annotations *) - let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in + let _ = Pretyping.understand_tcc Evd.empty env r in (*msgerrnl (str "Typage OK");*) () with e -> (*msgerrnl (str "Warning: can't type")*) () end; let c = @@ -716,8 +715,7 @@ let transf_pattern env c = if Options.do_translate() then Constrextern.extern_rawconstr (Termops.vars_of_env env) (Constrintern.for_grammar - (Constrintern.interp_rawconstr_gen false Evd.empty env true ([],[])) - c) + (Constrintern.intern_gen false ~allow_soapp:true Evd.empty env) c) else c let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c) diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 1e4b261036..bfe948c53f 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -660,7 +660,7 @@ let rec pr_vernac = function in let ctx = List.rev ctx in (Environ.push_rel_context ctx env, ctx@params) | LocalRawDef ((_,na),c) -> - let c = Constrintern.judgment_of_rawconstr sigma env c in + let c = Constrintern.interp_constr_judgment sigma env c in let d = (na, Some c.Environ.uj_val, c.Environ.uj_type) in (Environ.push_rel d env,d::params)) (env0,[]) lparams in |