diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-24 13:55:50 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-24 13:55:50 +0000 |
| commit | 0db0531fde66678f60d54df60be1337a7f489000 (patch) | |
| tree | 009323904a2355e610f4735862eeec4d0bf28423 /contrib | |
| parent | 3fbfcfd052fd7e007d50c8ee19e44525f80577ac (diff) | |
Declarative language: fixed the generation of fixpoints for induction proofs.
Cleaner code: the guardedness bug is now corrected.
Added "trivial" to the automation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/cc/ccalgo.ml | 8 | ||||
| -rw-r--r-- | contrib/first-order/g_ground.ml4 | 5 |
2 files changed, 9 insertions, 4 deletions
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml index bc39910d5..b7ef89a3a 100644 --- a/contrib/cc/ccalgo.ml +++ b/contrib/cc/ccalgo.ml @@ -401,6 +401,7 @@ let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) = qe_rhs_valid=valid2}::state.quant let add_inst state (inst,int_subst) = + check_for_interrupt (); if state.rew_depth > 0 then let subst = build_subst (forest state) int_subst in let prfhead= mkVar inst.qe_hyp_id in @@ -724,7 +725,8 @@ let find_instances state = let _ = debug msgnl (str "Running E-matching algorithm ... "); try - while true do + while true do + check_for_interrupt (); do_match state res pb_stack done; anomaly "get out of here !" @@ -734,7 +736,9 @@ let find_instances state = let rec execute first_run state = debug msgnl (str "Executing ... "); try - while one_step state do () + while + check_for_interrupt (); + one_step state do () done; match check_disequalities state with None -> diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index 975acc1c8..e48d47d9d 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -112,8 +112,9 @@ END let default_declarative_automation gls = - tclORELSE - (Cctac.congruence_tac !congruence_depth []) + tclORELSE + (tclORELSE (Auto.h_trivial [] None) + (Cctac.congruence_tac !congruence_depth [])) (gen_ground_tac true (Some (tclTHEN default_solver |