From ecf68d1ed251e2c6b4abd9e97400d3ab009d2925 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 27 Apr 2008 16:15:34 +0000 Subject: - Backtrack sur option with_types suite à confusion sur l'utilisation des types des with-bindings dans la 8.1 [ceux-ci étaient déjà utilisés et ce qui est vraiment nouveau est que l'unification est maintenant celle de evarconv alors que c'était avant un mélange d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je renonce à maintenir la compatibilité (on se retrouve donc avec un exemple qui fonctionne différement dans TermsConv.v de CoLoR). - Robustesse accrue pour la nouvelle facilité de syntaxe de binding avec paramètre pour pose/set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/auto.ml | 1 - tactics/class_tactics.ml4 | 3 --- tactics/setoid_replace.ml | 2 -- tactics/tacticals.ml | 4 ++-- tactics/tactics.ml | 10 +++------- 5 files changed, 5 insertions(+), 15 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 111245e117..0b1f29dc3b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -586,7 +586,6 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = false; - use_types = false; modulo_delta = empty_transparent_state; } diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 72bc85c2f4..4319a1d3de 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -72,7 +72,6 @@ open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; - use_types = true; modulo_delta = var_full_transparent_state; } @@ -632,7 +631,6 @@ let decompose_setoid_eqhyp env sigma c left2right = let rewrite_unif_flags = { Unification.modulo_conv_on_closed_terms = None; Unification.use_metas_eagerly = true; - Unification.use_types = true; Unification.modulo_delta = empty_transparent_state; } @@ -641,7 +639,6 @@ let conv_transparent_state = (Idpred.empty, Cpred.full) let rewrite2_unif_flags = { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; Unification.use_metas_eagerly = true; - Unification.use_types = true; Unification.modulo_delta = empty_transparent_state; } diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index b5710c9666..dc8ff2b9cd 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1734,14 +1734,12 @@ let check_evar_map_of_evars_defs evd = let rewrite_unif_flags = { modulo_conv_on_closed_terms = None; use_metas_eagerly = true; - use_types = true; modulo_delta = empty_transparent_state; } let rewrite2_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; - use_types = true; modulo_delta = empty_transparent_state; } diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 1bd65ecdf6..dd8aa12941 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -329,7 +329,7 @@ let general_elim_then_using mk_elim ind indclause gl = let elim = mk_elim ind gl in (* applying elimination_scheme just a little modified *) - let indclause' = clenv_match_args true indbindings indclause in + let indclause' = clenv_match_args indbindings indclause in let elimclause = mk_clenv_from gl (elim,pf_type_of gl elim) in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with @@ -350,7 +350,7 @@ let general_elim_then_using mk_elim error ("The elimination combinator " ^ name_elim ^ " is not known") in let elimclause' = clenv_fchain indmv elimclause indclause' in - let elimclause' = clenv_match_args true elimbindings elimclause' in + let elimclause' = clenv_match_args elimbindings elimclause' in let branchsigns = compute_construtor_signatures isrec ind in let brnames = compute_induction_names (Array.length branchsigns) allnames in let after_tac ce i gl = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cd8ad4c14d..d3f7cc5f15 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -551,7 +551,6 @@ let last_arg c = match kind_of_term c with let elim_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly = true; - use_types = true; modulo_delta = empty_transparent_state; } @@ -673,10 +672,9 @@ let simplest_case c = general_case_analysis false (c,NoBindings) (* Resolution with missing arguments *) -let general_apply with_delta_and_types with_destruct with_evars (c,lbind) gl = +let general_apply with_delta with_destruct with_evars (c,lbind) gl = let flags = - if with_delta_and_types then default_unify_flags - else simple_apply_unify_flags in + if with_delta then default_unify_flags else default_no_delta_unify_flags in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) @@ -686,9 +684,7 @@ let general_apply with_delta_and_types with_destruct with_evars (c,lbind) gl = let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in if n<0 then error "Apply: theorem has not enough premisses."; - let clause = - make_clenv_binding_apply with_delta_and_types (Some n) gl (c,thm_ty) lbind - in + let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in try try_apply thm_ty0 concl_nprod with PretypeError _|RefinerError _|UserError _|Failure _ as exn -> -- cgit v1.2.3