From 61379c8030304072ab347400718e1ef25762df80 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jun 2008 14:00:37 +0000 Subject: [PATCH] Bug fixed: wrong default pattern for generalize. --- helm/software/components/tactics/primitiveTactics.ml | 4 ++-- helm/software/components/tactics/tactics.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 7014a5941..7b58517f6 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -618,7 +618,7 @@ let generalize_tac = let module PET = ProofEngineTypes in let generalize_tac mk_fresh_name_callback - ~pattern:(term,hyps_pat,concl_pat) status + ~pattern:(term,hyps_pat,_) status = if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet; let (proof, goal) = status in @@ -743,7 +743,7 @@ let generalize_pattern_tac pattern = List.map (fun id -> let rel,_ = ProofEngineHelpers.find_hyp id context in - id,(Some (PET.const_lazy_term rel), [], None) + id,(Some (PET.const_lazy_term rel), [], Some (ProofEngineTypes.hole)) ) generalize_hyps in let tactics = List.map diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index c75f183e4..08b32e571 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Sat Jun 7 20:09:50 CEST 2008 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Jun 8 15:54:21 CEST 2008 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : -- 2.39.2