From f39cd683cb022d877a0d2ebd014fa0879bc6de00 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 6 Dec 2004 11:28:22 +0000 Subject: Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tactiques d'appliquer une éventuelle coercion vers le but MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/argextend.ml4 | 6 +++--- parsing/g_tactic.ml4 | 6 +++--- parsing/g_tacticnew.ml4 | 6 +++--- parsing/pcoq.ml4 | 6 +++--- parsing/pcoq.mli | 2 +- parsing/pptactic.ml | 9 +++------ parsing/q_coqast.ml4 | 2 +- 7 files changed, 17 insertions(+), 20 deletions(-) (limited to 'parsing') 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$ >> diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 5ba7d591e..97f5d46a9 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -42,7 +42,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if !Options.v7 then GEXTEND Gram GLOBAL: simple_tactic constrarg bindings constr_with_bindings - quantified_hypothesis red_expr int_or_var castedopenconstr + quantified_hypothesis red_expr int_or_var openconstr simple_intropattern; int_or_var: @@ -96,8 +96,8 @@ GEXTEND Gram | IDENT "Check"; c = constr -> ConstrTypeOf c | c = constr -> ConstrTerm c ] ] ; - castedopenconstr: - [ [ c = constr -> c ] ] + openconstr: + [ [ c = constr -> ((),c) ] ] ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 8930c8dca..70729ce13 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -109,7 +109,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if not !Options.v7 then GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis - bindings red_expr int_or_var castedopenconstr simple_intropattern; + bindings red_expr int_or_var openconstr simple_intropattern; int_or_var: [ [ n = integer -> Genarg.ArgArg n @@ -128,8 +128,8 @@ GEXTEND Gram | id = METAIDENT -> MetaId (loc,id) ] ] ; - castedopenconstr: - [ [ c = constr -> c ] ] + openconstr: + [ [ c = constr -> ((),c) ] ] ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 081d7aeec..496b6594d 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -371,8 +371,8 @@ module Tactic = (* Entries that can be refered via the string -> Gram.Entry.e table *) (* Typically for tactic user extensions *) - let castedopenconstr = - make_gen_entry utactic rawwit_casted_open_constr "castedopenconstr" + let openconstr = + make_gen_entry utactic rawwit_open_constr "openconstr" let constr_with_bindings = make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings" let bindings = @@ -418,7 +418,7 @@ let reset_all_grammars () = f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern; f Module.module_expr; f Module.module_type; f Tactic.simple_tactic; - f Tactic.castedopenconstr; + f Tactic.openconstr; f Tactic.constr_with_bindings; f Tactic.bindings; f Tactic.constrarg; diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index c2f1c0240..76c23ad20 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -156,7 +156,7 @@ module Module : module Tactic : sig open Rawterm - val castedopenconstr : constr_expr Gram.Entry.e + val openconstr : open_constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e val bindings : constr_expr bindings Gram.Entry.e val constrarg : (constr_expr,reference) may_eval Gram.Entry.e diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3057e41a4..76c9847ef 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -272,8 +272,7 @@ let rec pr_raw_generic prc prlc prtac prref x = pr_arg (pr_red_expr (prc,prref)) (out_gen rawwit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x) - | CastedOpenConstrArgType -> - pr_arg prc (out_gen rawwit_casted_open_constr x) + | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) | BindingsArgType -> @@ -320,8 +319,7 @@ let rec pr_glob_generic prc prlc prtac x = pr_arg (pr_red_expr (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x) - | CastedOpenConstrArgType -> - pr_arg prc (out_gen globwit_casted_open_constr x) + | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x) | BindingsArgType -> @@ -367,8 +365,7 @@ let rec pr_generic prc prlc prtac x = | RedExprArgType -> pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen wit_tactic x) - | CastedOpenConstrArgType -> - pr_arg prc (snd (out_gen wit_casted_open_constr x)) + | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) | BindingsArgType -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index e1bb51dd7..a4c58aec9 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -272,7 +272,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.HypArgType -> <:expr< Genarg.HypArgType >> | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> - | Genarg.CastedOpenConstrArgType -> <:expr< Genarg.CastedOpenConstrArgType >> + | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >> | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> -- cgit v1.2.3