From 700e8726d8b97f923ed7e02f1146a9787bde2333 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Michele=20Galat=C3=A0?= <??>
Date: Thu, 12 Dec 2002 15:36:00 +0000
Subject: [PATCH] Added an almost working version of Generalize tactic.
---
helm/gTopLevel/variousTactics.ml | 15 ++++-----------
1 file changed, 4 insertions(+), 11 deletions(-)
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?
-
-*)
--
2.39.5