]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: "by ... we proved ... that is equivalent to ...": the is equivalent
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Sep 2006 15:29:40 +0000 (15:29 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Sep 2006 15:29:40 +0000 (15:29 +0000)
to part was not considered because of a stupid typo.

helm/software/components/tactics/declarative.ml

index 4a7d3e52c6329263d838cf063b6aa9020743d051..4dcf38b6d56fc6f032fb00bc9aa62481906c6a44 100644 (file)
@@ -55,8 +55,8 @@ let by_term_we_proved ~dbd t ty id ty' =
    match ty' with
       None -> Tacticals.id_tac
     | Some ty' ->
-       Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
-        (fun _ metasenv ugraph -> ty,metasenv,ugraph)
+        Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+         (fun _ metasenv ugraph -> ty',metasenv,ugraph)
   in
    Tacticals.thens
    ~start: