aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml5
-rw-r--r--plugins/cc/ccalgo.mli9
-rw-r--r--plugins/cc/ccproof.ml3
-rw-r--r--plugins/cc/ccproof.mli3
-rw-r--r--plugins/cc/cctac.ml15
-rw-r--r--plugins/cc/cctac.mli1
-rw-r--r--plugins/cc/g_congruence.ml43
7 files changed, 17 insertions, 22 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 5c7cad7ff5..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
@@ -270,7 +269,7 @@ type state =
mutable rew_depth:int;
mutable changed:bool;
by_type: Int.Set.t Typehash.t;
- mutable gls:Proof_type.goal Evd.sigma}
+ mutable gls:Goal.goal Evd.sigma}
let dummy_node =
{
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 505029992a..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
@@ -129,7 +128,7 @@ val axioms : forest -> (term * term) Constrhash.t
val epsilons : forest -> pa_constructor list
-val empty : int -> Proof_type.goal Evd.sigma -> state
+val empty : int -> Goal.goal Evd.sigma -> state
val add_term : state -> term -> int
@@ -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..fca7d9851f 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
@@ -85,7 +84,8 @@ let rec decompose_term env sigma t=
| Proj (p, c) ->
let canon_const kn = Constant.make1 (Constant.canonical kn) in
let p' = Projection.map canon_const p in
- (Appli (Symb (Term.mkConst (Projection.constant p')), decompose_term env sigma c))
+ let c = Retyping.expand_projection env sigma p' c [] in
+ decompose_term env sigma c
| _ ->
let t = Termops.strip_outer_cast sigma t in
if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
@@ -232,7 +232,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)
@@ -441,11 +442,11 @@ let cc_tactic depth additionnal_terms =
let open Glob_term in
let env = Proofview.Goal.env gl in
let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
- let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
+ let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
let pr_missing (c, missing) =
- let c = Detyping.detype ~lax:true false [] env sigma c in
+ let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in
let holes = List.init missing (fun _ -> hole) in
- Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes))
+ Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
in
Feedback.msg_info
(Pp.str "Goal is solvable by congruence but some arguments are missing.");
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-03 19:43:05 +0000