diff options
| author | corbinea | 2003-10-16 15:44:47 +0000 |
|---|---|---|
| committer | corbinea | 2003-10-16 15:44:47 +0000 |
| commit | 8b5f6f835be01b2b0510cdbea939050d2c2583c6 (patch) | |
| tree | dca1d522a0845397fa13344ec771cadd1b27caba /contrib/linear/dpc.ml4 | |
| parent | 5f116846807c7cc6c5b58b13158f26505e558f2c (diff) | |
Ground update + Linear removal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4654 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/linear/dpc.ml4')
| -rwxr-xr-x | contrib/linear/dpc.ml4 | 64 |
1 files changed, 0 insertions, 64 deletions
diff --git a/contrib/linear/dpc.ml4 b/contrib/linear/dpc.ml4 deleted file mode 100755 index d30cf9ae1c..0000000000 --- a/contrib/linear/dpc.ml4 +++ /dev/null @@ -1,64 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -(*i $Id$ i*) - -open Pp -open Util - -open Proof_trees -open Tacmach -open Tactics -open Tacinterp -open Tacticals -open Prove -open Ccidpc - -let rec intros_forall gls = - let t = pf_concl gls - in if is_forall_term t - then ((tclTHEN intro (intros_forall))) gls - else tclIDTAC gls - -let dPC_nq gls = - let f = dpc_of_cci_fmla gls (pf_concl gls) in - try let pf = prove_f f in - tradpf [] [] pf gls - with Not_provable_in_DPC s -> errorlabstrm "dpc__DPC_nq" - (str "Not provable in Direct Predicate Calculus") - - | No_intuitionnistic_proof n -> errorlabstrm "dpc__DPC_nq" - ((str "Found ") ++ - (str (string_of_int n)) ++ - (str " classical proof(s) but no intuitionnistic one !")) - - -let dPC = - ((tclTHEN (intros_forall) (dPC_nq))) - - -let dPC_l lcom = - (tclTHEN (intros_forall) - (tclTHEN (generalize lcom) (dPC))) - -(* -let dPC_tac = hide_atomic_tactic "DPC" dPC - -let dPC_l_tac = hide_tactic "DPC_l" - (fun lcom -> dPC_l lcom) -*) - -TACTIC EXTEND Linear -[ "Linear" ]->[(dPC)] -|[ "Linear" "with" ne_constr_list(l) ] -> [(dPC_l l)] -END - - - |