aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml29
-rw-r--r--plugins/cc/ccalgo.mli4
-rw-r--r--plugins/cc/ccproof.ml2
-rw-r--r--plugins/cc/ccproof.mli2
-rw-r--r--plugins/cc/cctac.ml8
5 files changed, 23 insertions, 22 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 1828213227..ccef9ab960 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 Sorts
+open Constr
open Vars
-open Tacmach
open Evd
+open Goptions
+open Tacmach
+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
@@ -436,9 +437,9 @@ and make_app l=function
and applist_proj c l =
match c with
| Symb s -> applist_projection s l
- | _ -> applistc (constr_of_term c) l
+ | _ -> Term.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
@@ -446,15 +447,15 @@ and applist_projection c l =
let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *)
let pb = Environ.lookup_projection p (Global.env()) in
let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in
- it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
+ Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx
| hd :: tl ->
- applistc (mkProj (p, hd)) tl)
- | _ -> applistc c l
+ Term.applistc (mkProj (p, hd)) tl)
+ | _ -> Term.applistc 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))
@@ -837,7 +838,7 @@ let complete_one_class state i=
let _args =
List.map (fun i -> constr_of_term (term state.uf i))
pac.args in
- let typ = prod_applist _c (List.rev _args) in
+ let typ = Term.prod_applist _c (List.rev _args) in
let ct = app (term state.uf i) typ pac.arity in
state.uf.epsilons <- pac :: state.uf.epsilons;
ignore (add_term state ct)
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index f904aa3e68..23cd2161d7 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 a43a167e86..97efaced8f 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 9f53123db1..a3e4501342 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 150319f6b9..8642df6846 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -12,7 +12,7 @@ open Evd
open Names
open Inductiveops
open Declarations
-open Term
+open Constr
open EConstr
open Vars
open Tactics
@@ -76,11 +76,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 +198,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:34:41 +0000