From: Claudio Sacerdoti Coen Date: Tue, 21 Aug 2007 09:48:14 +0000 (+0000) Subject: "obtain H E1=E2 by proof" is now working X-Git-Tag: 0.4.95@7852~262 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c84403b0c5272eb44adafa48ffaf6abdc637fc65;p=helm.git "obtain H E1=E2 by proof" is now working --- diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 8e077c6bd..c248d0cad 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -171,7 +171,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = in let ty,_ = CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in - let just = + let just' = match just with `Auto params -> let params = @@ -246,8 +246,9 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal) in let goals = - match goals with - [g1;g2] -> [g2;newmeta;g1] + match just,goals with + `Proof, [g1;g2;g3] -> [g2;g3;newmeta;g1] + | _, [g1;g2] -> [g2;newmeta;g1] | _ -> assert false in proof,goals) @@ -255,11 +256,11 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = let continuation = if last_step then (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*) - just + just' else Tacticals.thens ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs])) - ~continuations:[just ; Tacticals.id_tac] + ~continuations:[just' ; Tacticals.id_tac] in prepare continuation in