diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-09 21:06:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-09 21:06:39 +0000 |
| commit | 9c73559b6c7f578e2e7513971f27cf81fc9bfd06 (patch) | |
| tree | a7e530492c94f07a69cc683f3b2a5e5418ff0b1f /interp | |
| parent | f99bc7317fa0746b0ffebaf48656b2c0be351312 (diff) | |
Restauration type casted_open_constr pour tactique refine car l'unification n'est pas assez puissante pour retarder la coercion vers le but au dernier moment
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.ml | 16 | ||||
| -rw-r--r-- | interp/genarg.mli | 10 |
2 files changed, 21 insertions, 5 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml index 3483695ec..2b01a2034 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -34,7 +34,7 @@ type argument_type = | ConstrMayEvalArgType | QuantHypArgType | TacticArgType - | OpenConstrArgType + | OpenConstrArgType of bool | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType @@ -144,9 +144,17 @@ let rawwit_tactic = TacticArgType let globwit_tactic = TacticArgType let wit_tactic = TacticArgType -let rawwit_open_constr = OpenConstrArgType -let globwit_open_constr = OpenConstrArgType -let wit_open_constr = OpenConstrArgType +let rawwit_open_constr_gen b = OpenConstrArgType b +let globwit_open_constr_gen b = OpenConstrArgType b +let wit_open_constr_gen b = OpenConstrArgType b + +let rawwit_open_constr = rawwit_open_constr_gen false +let globwit_open_constr = globwit_open_constr_gen false +let wit_open_constr = wit_open_constr_gen false + +let rawwit_casted_open_constr = rawwit_open_constr_gen true +let globwit_casted_open_constr = globwit_open_constr_gen true +let wit_casted_open_constr = wit_open_constr_gen true let rawwit_constr_with_bindings = ConstrWithBindingsArgType let globwit_constr_with_bindings = ConstrWithBindingsArgType diff --git a/interp/genarg.mli b/interp/genarg.mli index 7f01cd6ac..af02a9ebe 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -132,10 +132,18 @@ val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta) val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type val wit_constr_may_eval : (constr,constr,'ta) abstract_argument_type +val rawwit_open_constr_gen : bool -> (open_constr_expr,constr_expr,'ta) abstract_argument_type +val globwit_open_constr_gen : bool -> (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type +val wit_open_constr_gen : bool -> (open_constr,constr,'ta) abstract_argument_type + val rawwit_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type val wit_open_constr : (open_constr,constr,'ta) abstract_argument_type +val rawwit_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type +val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type +val wit_casted_open_constr : (open_constr,constr,'ta) abstract_argument_type + val rawwit_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type 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 @@ -227,7 +235,7 @@ type argument_type = | ConstrMayEvalArgType | QuantHypArgType | TacticArgType - | OpenConstrArgType + | OpenConstrArgType of bool | ConstrWithBindingsArgType | BindingsArgType | RedExprArgType |