From 4da48b01f420d8eccf6dcb2fea11bb4d9f8d8a86 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 May 2003 22:38:38 +0000
Subject: Suppression définitive de lmatch et or_metanum dans tacinterp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 43785836af..9be6eb3932 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -726,7 +726,7 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
     if onlyparse then None
     else
       let r = interp_rawconstr_gen
-          false Evd.empty (Global.env()) [] (Some []) (vars,[]) c in
+          false Evd.empty (Global.env()) [] false (vars,[]) c in
       Some (make_old_pp_rule ppn ppsymbols pptyps r notation scope vars) in
   (* Declare the interpretation *)
   let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
@@ -802,7 +802,7 @@ let add_notation local df c modifiers mv8 sc =
 		let onlyparse = modifiers = [SetOnlyParsing] in
 		let a = interp_aconstr vars c in
 		let a_for_old = interp_rawconstr_gen
-		  false Evd.empty (Global.env()) [] (Some []) (vars,[]) c in
+		  false Evd.empty (Global.env()) [] false (vars,[]) c in
 		add_notation_interpretation_core local vars symbs df
 		  (a,a_for_old) sc onlyparse
 	  | Some n ->
-- 
cgit v1.2.3