From 9b610cc3493997088546be5225f74aa2abd3759c Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 8 Jun 2006 20:23:17 +0000 Subject: Changement du type d'argument 'TacticArgType X' en un type 'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/debug_tac.ml4 | 6 +++--- contrib/interface/xlate.ml | 14 ++++++++------ 2 files changed, 11 insertions(+), 9 deletions(-) (limited to 'contrib/interface') diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index 56abfb82b5..e1b8e7125e 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -239,9 +239,9 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti by the list of integers given as extra arguments. *) -let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level -let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level -let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level +let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level +let globwit_main_tactic = Pcoq.globwit_tactic Pcoq.tactic_main_level +let wit_main_tactic = Pcoq.wit_tactic Pcoq.tactic_main_level let on_then = function [t1;t2;l] -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 585e4bfb65..ecb04e0755 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -682,7 +682,7 @@ let xlate_with_names = function IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp) -let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level +let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) = function @@ -1271,14 +1271,15 @@ and coerce_genarg_to_TARG x = (CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x))) | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument" | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument" - | TacticArgType n -> - let t = xlate_tactic (out_gen (rawwit_tactic n) x) in - CT_coerce_TACTIC_COM_to_TARG t | OpenConstrArgType b -> CT_coerce_SCOMMENT_CONTENT_to_TARG (CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula (snd (out_gen (rawwit_open_constr_gen b) x)))) + | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> + let n = out_some (Pcoq.tactic_genarg_level s) in + let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in + CT_coerce_TACTIC_COM_to_TARG t | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" | BindingsArgType -> xlate_error "TODO: generic with bindings" | RedExprArgType -> xlate_error "TODO: generic red expr" @@ -1368,8 +1369,9 @@ let coerce_genarg_to_VARG x = (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x))) | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument" | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument" - | TacticArgType n -> - let t = xlate_tactic (out_gen (rawwit_tactic n) x) in + | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> + let n = out_some (Pcoq.tactic_genarg_level s) in + let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t) | OpenConstrArgType _ -> xlate_error "TODO: generic open constr" | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" -- cgit v1.2.3