From: Ferruccio Guidi Date: Fri, 20 Jul 2007 14:48:36 +0000 (+0000) Subject: acic_procedural: bug fix: X-Git-Tag: make_still_working~6145 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=58c0db9bcf83591115445a538bee028d3260fdf7;p=helm.git acic_procedural: bug fix: sometimes whd is not enough, we need normalize ... --- diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index 489feb4b6..4c0014d2e 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.ml +++ b/helm/software/components/acic_procedural/proceduralClassify.ml @@ -78,7 +78,7 @@ let classify_conclusion vs = let classify c t = try - let vs, h = PEH.split_with_whd (c, t) in + let vs, h = PEH.split_with_normalize (c, t) in let rc = classify_conclusion vs in let map (b, h) (c, v) = let _, argsno = PEH.split_with_whd (c, v) in diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index 85dba95ea..ec2e1919c 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -652,6 +652,13 @@ let split_with_whd (c, t) = in aux false [] 0 c t +let split_with_normalize (c, t) = + let add s v c = Some (s, Cic.Decl v) :: c in + let rec aux a n c = function + | Cic.Prod (s, v, t) -> aux ((c, v) :: a) (succ n) (add s v c) t + | v -> (c, v) :: a, n + in + aux [] 0 c (CicReduction.normalize c t) (* menv sorting *) module OT = diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli index 1eeb0aca3..39fb69b0d 100644 --- a/helm/software/components/tactics/proofEngineHelpers.mli +++ b/helm/software/components/tactics/proofEngineHelpers.mli @@ -121,6 +121,10 @@ val get_rel: Cic.context -> string -> Cic.term option t and t_i is the premise of t accessed by Rel i in t_0. Performes a whd on the conclusion before giving up. Each t_i is returned with a context c_i in wich it is typed + split_with_normalize (c, t) normalizes t before operating the split + whd is useless here *) val split_with_whd: Cic.context * Cic.term -> (Cic.context * Cic.term) list * int +val split_with_normalize: Cic.context * Cic.term -> + (Cic.context * Cic.term) list * int