aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate
diff options
context:
space:
mode:
Diffstat (limited to 'translate')
-rw-r--r--translate/ppconstrnew.ml5
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