aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml3
-rw-r--r--plugins/cc/ccalgo.mli7
-rw-r--r--plugins/cc/ccproof.ml3
-rw-r--r--plugins/cc/ccproof.mli3
-rw-r--r--plugins/cc/cctac.ml6
-rw-r--r--plugins/cc/cctac.mli1
-rw-r--r--plugins/cc/g_congruence.ml43
7 files changed, 10 insertions, 16 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..11d3a6d1f4 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
@@ -232,7 +231,8 @@ let make_prb gls depth additionnal_terms =
let build_projection intype (cstr:pconstructor) special default gls=
let open Tacmach.New in
let ci= (snd(fst cstr)) in
- let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+ let sigma = project gls in
+ let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in
let id=pf_get_new_id (Id.of_string "t") gls in
sigma, mkLambda(Name id,intype,body)
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:09:53 +0000