From 26a7213e85f3dcba8135215c0389b8d1056a43df Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 8 Oct 2003 15:15:52 +0000 Subject: Des abbreviations pour constrintern.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4546 85f007b7-540e-0410-9357-904b9bb8a0f7 --- translate/ppconstrnew.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'translate') 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 -- cgit v1.2.3