diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 3 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 7 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 3 | ||||
| -rw-r--r-- | plugins/cc/ccproof.mli | 3 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 3 | ||||
| -rw-r--r-- | plugins/cc/cctac.mli | 1 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 3 |
7 files changed, 8 insertions, 15 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 39fb8feeb8..1828213227 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,6 @@ (* Downey,Sethi and Tarjan. *) (* Plus some e-matching and constructor handling by P. Corbineau *) -open API open CErrors open Util open Pp diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 51e2301fe6..f904aa3e68 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Term open Names @@ -121,7 +120,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (unit -> Pp.std_ppcmds) -> unit +val debug : (unit -> Pp.t) -> unit val forest : state -> forest @@ -170,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option -val pr_idx_term : forest -> int -> Pp.std_ppcmds +val pr_idx_term : forest -> int -> Pp.t val empty_forest: unit -> forest diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index eecb7bc983..a43a167e86 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,6 @@ (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) -open API open CErrors open Term open Ccalgo diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 4e4d42f869..9f53123db1 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ccalgo open Term diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0f5b806644..4934b0750b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ (* This file is the interface between the c-c algorithm and Coq *) -open API open Evd open Names open Inductiveops diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index ef32d2b83e..b4bb62be8e 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr val proof_tac: Ccproof.proof -> unit Proofview.tactic diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 43b150c346..6ed4672ce3 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Cctac open Stdarg |