diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-13 18:47:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-13 18:47:49 +0000 |
| commit | 34ba48a885c91ea895cbba7ba5a53b1ec9de5db8 (patch) | |
| tree | 7c793d76af431bc2cb0aa78e7e9edaa991d1892f /interp/constrintern.mli | |
| parent | 6e9c0edd9efc9d72e6f32bc434a34076b1a6afee (diff) | |
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
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 12aaeec17..1af6854d3 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 *) |