From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- plugins/cc/ccalgo.ml | 13 +++++++------ plugins/cc/ccalgo.mli | 4 ++-- plugins/cc/ccproof.ml | 2 +- plugins/cc/ccproof.mli | 2 +- plugins/cc/cctac.ml | 7 ++++--- 5 files changed, 15 insertions(+), 13 deletions(-) (limited to 'plugins/cc') diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 182821322..faabd7c14 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -11,14 +11,15 @@ (* Plus some e-matching and constructor handling by P. Corbineau *) open CErrors -open Util open Pp open Goptions open Names open Term +open Constr open Vars open Tacmach open Evd +open Util let init_size=5 @@ -154,7 +155,7 @@ let rec term_equal t1 t2 = open Hashset.Combine let rec hash_term = function - | Symb c -> combine 1 (hash_constr c) + | Symb c -> combine 1 (Constr.hash c) | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) @@ -215,7 +216,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality @@ -232,7 +233,7 @@ type node = module Constrhash = Hashtbl.Make (struct type t = constr let equal = eq_constr_nounivs - let hash = hash_constr + let hash = Constr.hash end) module Typehash = Constrhash @@ -438,7 +439,7 @@ and applist_proj c l = | Symb s -> applist_projection s l | _ -> applistc (constr_of_term c) l and applist_projection c l = - match kind_of_term c with + match Constr.kind c with | Const c when Environ.is_projection (fst c) (Global.env()) -> let p = Projection.make (fst c) false in (match l with @@ -454,7 +455,7 @@ and applist_projection c l = let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in let func c = canonize_name sigma (EConstr.of_constr c) in - match kind_of_term c with + match Constr.kind c with | Const (kn,u) -> let canon_const = Constant.make1 (Constant.canonical kn) in (mkConstU (canon_const,u)) diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index f904aa3e6..23cd2161d 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -7,7 +7,7 @@ (************************************************************************) open Util -open Term +open Constr open Names type pa_constructor = @@ -85,7 +85,7 @@ type representative= mutable lfathers:Int.Set.t; mutable fathers:Int.Set.t; mutable inductive_status: inductive_status; - class_type : Term.types; + class_type : types; mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *) type cl = Rep of representative| Eqto of int*equality diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index a43a167e8..97efaced8 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -10,7 +10,7 @@ (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open CErrors -open Term +open Constr open Ccalgo open Pp diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 9f53123db..a3e450134 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -7,7 +7,7 @@ (************************************************************************) open Ccalgo -open Term +open Constr type rule= Ax of constr diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 150319f6b..7dec34d4d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -13,6 +13,7 @@ open Names open Inductiveops open Declarations open Term +open Constr open EConstr open Vars open Tactics @@ -76,11 +77,11 @@ let rec decompose_term env sigma t= let (mind,i_ind),u = c in let u = EInstance.kind sigma u in let canon_mind = MutInd.make1 (MutInd.canonical mind) in - let canon_ind = canon_mind,i_ind in (Symb (Term.mkIndU (canon_ind,u))) + let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) | Const (c,u) -> let u = EInstance.kind sigma u in let canon_const = Constant.make1 (Constant.canonical c) in - (Symb (Term.mkConstU (canon_const,u))) + (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> let canon_const kn = Constant.make1 (Constant.canonical kn) in let p' = Projection.map canon_const p in @@ -198,7 +199,7 @@ let make_prb gls depth additionnal_terms = (fun decl -> let id = NamedDecl.get_id decl in begin - let cid=Term.mkVar id in + let cid=Constr.mkVar id in match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b -- cgit v1.2.3