From 82d4772ee9ac860f0a99b774612d2cf19838bb4b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 27 May 2009 06:38:45 +0000 Subject: [PATCH] Avoiding to filter the application of congruence equations due to a couple of cases in "didactics" where auto is used instead of reflexivity. --- helm/software/components/tactics/auto.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 34b305ba5..973cc1d78 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1037,7 +1037,7 @@ let apply_smart_aux in match Saturation.solve_narrowing bag (proof'''',newmeta) active passive - 1 (*0 infinity*) + 2 (*0 infinity*) with | None, active, passive, bag -> raise (ProofEngineTypes.Fail (lazy ("paramod fails"))) @@ -1645,12 +1645,12 @@ let applicative_case dbd let candidates = get_candidates flags.skip_trie_filtering universe cache goalty_aux in - (* if the goal is an equality we skip the congruence theorems *) + (* if the goal is an equality we skip the congruence theorems let candidates = if is_equational_case goalty flags - then List.filter not_default_eq_term candidates - else candidates - in + then List.filter not_default_eq_term candidates + else candidates + in *) let candidates = List.filter (only signature context metasenv) candidates in let tables, elems = -- 2.39.2