diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 15:15:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-08 15:15:52 +0000 |
| commit | 26a7213e85f3dcba8135215c0389b8d1056a43df (patch) | |
| tree | 1fb05753a289c02c21ea5f2c8ccddfd7ac20608c /translate | |
| parent | 12b8bbd43c90456c3f4a586ac9f67b9d1972cd71 (diff) | |
Des abbreviations pour constrintern.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 3b4f3296c..03e83caca 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -577,8 +577,7 @@ let transf istype env n iscast c = if Options.do_translate() then let r = Constrintern.for_grammar - (Constrintern.interp_rawconstr_gen istype Evd.empty env [] false - ([],[])) + (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[])) c in begin try (* Try to infer old case and type annotations *) @@ -608,7 +607,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 ([],[])) + (Constrintern.interp_rawconstr_gen false Evd.empty env true ([],[])) c) else c |