diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 11:28:22 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 11:28:22 +0000 |
| commit | f39cd683cb022d877a0d2ebd014fa0879bc6de00 (patch) | |
| tree | 1c691cb8f07513c905045b7b70d52872ed5e69dc /parsing/argextend.ml4 | |
| parent | c81e081287075310f78081728d4a6359f6ff017a (diff) | |
Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tactiques d'appliquer une éventuelle coercion vers le but
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/argextend.ml4')
| -rw-r--r-- | parsing/argextend.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index df48f5d8d..78128a99d 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -33,7 +33,7 @@ let rec make_rawwit loc = function | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> | TacticArgType -> <:expr< Genarg.rawwit_tactic >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.rawwit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.rawwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> @@ -59,7 +59,7 @@ let rec make_globwit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.globwit_tactic >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.globwit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.globwit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> @@ -85,7 +85,7 @@ let rec make_wit loc = function | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> | TacticArgType -> <:expr< Genarg.wit_tactic >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >> + | OpenConstrArgType -> <:expr< Genarg.wit_open_constr >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Genarg.wit_bindings >> | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> |