diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-09 12:21:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-09 12:21:04 +0000 |
| commit | 3588bde12b2b8d531b3b2ffde7e79d32c3acd040 (patch) | |
| tree | 173dc02b07f6cc9407e5d75763e140d63b5a06ed /tactics | |
| parent | 16ea6252339bed9901fff48b5883f4d471a88e7a (diff) | |
Turning tauto into a classical tautology prover as soon as classical
logic (file Classical_Prop.v) is loaded.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12077 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tauto.ml4 | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 3f5b0a4a3..0e14c471a 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -245,12 +245,25 @@ let intuition_gen tac = let simplif_gen = interp (tacticIn simplif) -let tauto g = +let tauto_intuitionistic g = try intuition_gen <:tactic<fail>> g with Refiner.FailError _ | UserError _ -> errorlabstrm "tauto" (str "tauto failed.") +let coq_nnpp_path = + let dir = List.map id_of_string ["Classical_Prop";"Logic";"Coq"] in + Libnames.make_path (make_dirpath dir) (id_of_string "NNPP") + +let tauto_classical g = + try + let nnpp = constr_of_global (Nametab.absolute_reference coq_nnpp_path) in + tclTHEN (apply nnpp) tauto_intuitionistic g + with Not_found -> + tclIDTAC g + +let tauto = tclORELSE tauto_intuitionistic tauto_classical + let default_intuition_tac = <:tactic< auto with * >> TACTIC EXTEND tauto |