From: Michele Galatà <??>
Date: Thu, 12 Dec 2002 15:36:00 +0000 (+0000)
Subject: Added an almost working version of Generalize tactic.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=700e8726d8b97f923ed7e02f1146a9787bde2333;p=helm.git

Added an almost working version of Generalize tactic.
---

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index 7d0748385..615cf43b4 100644
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -74,15 +74,15 @@ let generalize_tac ~term ~status:((proof,goal) as status) =
      T.thens 
       ~start:(P.cut_tac 
        ~term:(
-         C.Prod (
-          (C.Name "dummy_for_gen")), 
-          (CicTypeChecker.type_of_aux' metasenv context term)),
+         C.Prod(
+          (C.Name "dummy_for_gen"), 
+          (CicTypeChecker.type_of_aux' metasenv context term),
           (ProofEngineReduction.replace_lifting_csc 1
             ~equality:(==) 
             ~what:term 
             ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)  
             ~where:ty)
-          )	
+          )))	
       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
       ~status
 ;;
@@ -112,10 +112,3 @@ let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
 ;;
 *)
 
-
-
-(*** DOMANDE ***
-
-- field, omega... come ring?
-
-*)