diff options
Diffstat (limited to 'contrib/rtauto/refl_tauto.mli')
| -rw-r--r-- | contrib/rtauto/refl_tauto.mli | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/contrib/rtauto/refl_tauto.mli b/contrib/rtauto/refl_tauto.mli deleted file mode 100644 index 480dbb30..00000000 --- a/contrib/rtauto/refl_tauto.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* $Id: refl_tauto.mli 7233 2005-07-15 12:34:56Z corbinea $ *) - -(* raises Not_found if no proof is found *) - -type atom_env= - {mutable next:int; - mutable env:(Term.constr*int) list} - -val make_form : atom_env -> - Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form - -val make_hyps : - atom_env -> - Proof_type.goal Tacmach.sigma -> - Term.types list -> - (Names.identifier * Term.types option * Term.types) list -> - (Names.identifier * Proof_search.form) list - -val rtauto_tac : Proof_type.tactic |