diff options
| author | corbinea | 2003-05-08 16:45:17 +0000 |
|---|---|---|
| committer | corbinea | 2003-05-08 16:45:17 +0000 |
| commit | 03c37b5fd14b32ad4096342f9295073253886f17 (patch) | |
| tree | 7f00166a34937833a2c3b1977dbc8b26635eec93 | |
| parent | 19d7e0ef6f45d918f5a2ebdbb4e634a4e4580cb2 (diff) | |
bugfixes in Ground.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3997 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/first-order/engine.ml4 | 2 | ||||
| -rw-r--r-- | contrib/first-order/rules.ml | 13 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 2 |
3 files changed, 10 insertions, 7 deletions
diff --git a/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4 index 26abbc63bb..07864fe9bf 100644 --- a/contrib/first-order/engine.ml4 +++ b/contrib/first-order/engine.ml4 @@ -27,6 +27,8 @@ open Util let ground_tac solver startseq gl= let rec toptac seq gl= + if Tacinterp.get_debug()=Tactic_debug.DebugOn + then Pp.msgnl (Proof_trees.pr_goal (sig_it gl)); match seq.gl with Atomic t-> tclORELSE (axiom_tac t seq) (left_tac seq []) gl diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index a35896069e..00a6fe89df 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -180,7 +180,7 @@ let ll_atom_tac a id tacrec seq= wrap 1 false tacrec seq] with Not_found->tclFAIL 0 "No link" -let ll_false_tac id tacrec seq= +let ll_false_tac id tacrec seq = tclTHEN (clear_global id) (wrap 0 false tacrec seq) let left_false_tac id= @@ -213,11 +213,12 @@ let ll_ind_tac ind largs id tacrec seq gl= let ll_forall_tac prod id tacrec seq= tclTHENS (cut prod) [tclTHENLIST - [(fun gls->generalize - [mkApp(constr_of_reference id, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); + [intro; + (fun gls-> + let id0=pf_nth_hyp_id gls 1 in + let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in + tclTHEN (generalize [term]) (clear [id0]) gls); clear_global id; intro; tclSOLVE [wrap 1 false tacrec (deepen seq)]]; - tclSOLVE [wrap 0 true tacrec (deepen seq)]] - + tclSOLVE [wrap 0 true tacrec (deepen seq)]] diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 40fe19b30f..678c35a950 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -24,7 +24,7 @@ let priority = function (* pure heuristics, <=0 for non reversible *) Lfalse ->1000 | Land _ -> 90 | Lor _ -> 40 - | Lforall (_,_) -> -30 + | Lforall (_,_) -> -30 (* must stay at lowest priority *) | Lexists -> 60 | Levaluable _ -> 100 | LA(_,lap) -> |