Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de

fonctionner entre la V7.3 et la V8.0 (notation : "@ ?meta id1 ... idn")



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9644 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 9 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0a42d2ba9b..244f8228a9 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -776,7 +776,7 @@ let reset_tmp_scope (ids,tmp_scope,scopes) =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalise sigma globalenv env allow_soapp lvar c =
+let internalise sigma globalenv env allow_patvar lvar c =
   let rec intern (ids,tmp_scope,scopes as env) = function
     | CRef ref as x ->
 	let (c,imp,subscopes,l) = intern_reference env lvar ref in
@@ -916,10 +916,8 @@ let internalise sigma globalenv env allow_soapp lvar c =
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
 	RHole (loc, Evd.QuestionMark)
-    | CPatVar (loc, n) when allow_soapp ->
+    | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
-    | CPatVar (loc, (false,n)) ->
-        error_unbound_patvar loc n
     | CPatVar (loc, _) ->
 	raise (InternalisationError (loc,NegativeMetavariable))
     | CEvar (loc, n) ->
@@ -1078,12 +1076,12 @@ let extract_ids env =
     Idset.empty
 
 let intern_gen isarity sigma env
-               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let tmp_scope = 
     if isarity then Some Notation.type_scope else None in
   internalise sigma env (extract_ids env, tmp_scope,[])
-    allow_soapp (ltacvars,Environ.named_context env, [], impls) c
+    allow_patvar (ltacvars,Environ.named_context env, [], impls) c
 
 let intern_constr sigma env c = intern_gen false sigma env c 
 
@@ -1102,10 +1100,10 @@ let intern_ltac isarity ltacvars sigma env c =
 (* Functions to parse and interpret constructions *)
 
 let interp_gen kind sigma env 
-               ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+               ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   Default.understand_gen kind sigma env 
-    (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c)
+    (intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c)
 
 let interp_constr sigma env c =
   interp_gen (OfType None) sigma env c 
@@ -1140,7 +1138,7 @@ let interp_constr_judgment_evars isevars env c =
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let interp_constrpattern sigma env c =
-  pattern_of_rawconstr (intern_gen false sigma env ~allow_soapp:true c)
+  pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c)
 
 let interp_aconstr impls vars a =
   let env = Global.env () in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 12aaeec17f..1af6854d3e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -52,7 +52,7 @@ type ltac_sign = identifier list * unbound_ltac_var_map
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 
 val intern_gen : bool -> evar_map -> env ->
-  ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
 
 val intern_pattern : env -> cases_pattern_expr ->
@@ -68,7 +68,7 @@ val intern_pattern : env -> cases_pattern_expr ->
 (* Main interpretation function *)
 
 val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> constr
 
 (* Particular instances *)