diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /plugins/cc/ccalgo.mli | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/cc/ccalgo.mli')
| -rw-r--r-- | plugins/cc/ccalgo.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 6232b126e..5d286c732 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -18,7 +18,7 @@ type cinfo = type term = Symb of constr | Product of sorts_family * sorts_family - | Eps of identifier + | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -87,7 +87,7 @@ val add_equality : state -> constr -> term -> term -> unit val add_disequality : state -> from -> term -> term -> unit -val add_quant : state -> identifier -> bool -> +val add_quant : state -> Id.t -> bool -> int * patt_kind * ccpattern * patt_kind * ccpattern -> unit val tail_pac : pa_constructor -> pa_constructor @@ -106,7 +106,7 @@ val join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list type quant_eq= - {qe_hyp_id: identifier; + {qe_hyp_id: Id.t; qe_pol: bool; qe_nvars:int; qe_lhs: ccpattern; @@ -161,7 +161,7 @@ type term = type rule = Congruence - | Axiom of Names.identifier + | Axiom of Names.Id.t | Injection of int*int*int*int type equality = @@ -207,19 +207,19 @@ val process_rec : UF.t -> equality list -> int list val cc : UF.t -> unit val make_uf : - (Names.identifier * (term * term)) list -> UF.t + (Names.Id.t * (term * term)) list -> UF.t val add_one_diseq : UF.t -> (term * term) -> int * int val add_disaxioms : - UF.t -> (Names.identifier * (term * term)) list -> - (Names.identifier * (int * int)) list + UF.t -> (Names.Id.t * (term * term)) list -> + (Names.Id.t * (int * int)) list val check_equal : UF.t -> int * int -> bool val find_contradiction : UF.t -> - (Names.identifier * (int * int)) list -> - (Names.identifier * (int * int)) + (Names.Id.t * (int * int)) list -> + (Names.Id.t * (int * int)) *) |