diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-01 15:36:05 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-01 15:36:05 +0000 |
| commit | 34f26b527c2bec59ed496760329603b20ea6e332 (patch) | |
| tree | f597ca512ec79d102d0c62d377d05eedbe34d87c /interp/genarg.mli | |
| parent | 1d5d6427e6ab85f925207ee099729932c669ab16 (diff) | |
Nouvelle tactique EExists
Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/genarg.mli')
| -rw-r--r-- | interp/genarg.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/genarg.mli b/interp/genarg.mli index 2418646d9..23e1b5377 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -60,7 +60,7 @@ ConstrMayEvalArgType constr_expr may_eval constr QuantHypArgType quantified_hypothesis quantified_hypothesis TacticArgType raw_tactic_expr tactic CastedOpenConstrArgType constr_expr open_constr -ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings +ConstrBindingsArgType constr_expr with_bindings constr with_bindings List0ArgType of argument_type List1ArgType of argument_type OptArgType of argument_type @@ -121,9 +121,9 @@ val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) ab val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type val wit_constr_with_bindings : (constr with_bindings,constr,'ta) abstract_argument_type -val rawwit_with_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type -val globwit_with_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type -val wit_with_bindings : (constr bindings,constr,'ta) abstract_argument_type +val rawwit_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type +val globwit_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type +val wit_bindings : (constr bindings,constr,'ta) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type @@ -208,7 +208,7 @@ type argument_type = | TacticArgType | CastedOpenConstrArgType | ConstrWithBindingsArgType - | WithBindingsArgType + | BindingsArgType | RedExprArgType | List0ArgType of argument_type | List1ArgType of argument_type |