summaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml98
-rw-r--r--plugins/cc/ccalgo.mli13
-rw-r--r--plugins/cc/ccproof.ml10
-rw-r--r--plugins/cc/ccproof.mli4
-rw-r--r--plugins/cc/cctac.ml47
-rw-r--r--plugins/cc/cctac.mli4
-rw-r--r--plugins/cc/g_congruence.ml44
7 files changed, 105 insertions, 75 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 3c40cfb9..e3d27f71 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* This file implements the basic congruence-closure algorithm by *)
(* Downey,Sethi and Tarjan. *)
@@ -30,6 +28,7 @@ let debug f x =
let _=
let gdopt=
{ optsync=true;
+ optdepr=false;
optname="Congruence Verbose";
optkey=["Congruence";"Verbose"];
optread=(fun ()-> !cc_verbose);
@@ -105,6 +104,26 @@ type term=
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
+let rec term_equal t1 t2 =
+ match t1, t2 with
+ | Symb c1, Symb c2 -> eq_constr c1 c2
+ | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2
+ | Eps i1, Eps i2 -> id_ord i1 i2 = 0
+ | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
+ | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
+ Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
+ i1 = i2 && j1 = j2 && eq_constructor c1 c2
+ | _ -> t1 = t2
+
+open Hashtbl_alt.Combine
+
+let rec hash_term = function
+ | Symb c -> combine 1 (hash_constr c)
+ | Product (s1, s2) -> combine3 2 (Hashtbl.hash s1) (Hashtbl.hash s2)
+ | Eps i -> combine 3 (Hashtbl.hash i)
+ | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
+ | Constructor {ci_constr=c; ci_arity=i; ci_nhyps=j} -> combine4 5 (Hashtbl.hash c) i j
+
type ccpattern =
PApp of term * ccpattern list (* arguments are reversed *)
| PVar of int
@@ -172,13 +191,32 @@ type node =
vertex:vertex;
term:term}
+module Constrhash = Hashtbl.Make
+ (struct type t = constr
+ let equal = eq_constr
+ let hash = hash_constr
+ end)
+module Typehash = Constrhash
+
+module Termhash = Hashtbl.Make
+ (struct type t = term
+ let equal = term_equal
+ let hash = hash_term
+ end)
+
+module Identhash = Hashtbl.Make
+ (struct type t = identifier
+ let equal = Pervasives.(=)
+ let hash = Hashtbl.hash
+ end)
+
type forest=
{mutable max_size:int;
mutable size:int;
mutable map: node array;
- axioms: (constr,term*term) Hashtbl.t;
+ axioms: (term*term) Constrhash.t;
mutable epsilons: pa_constructor list;
- syms:(term,int) Hashtbl.t}
+ syms: int Termhash.t}
type state =
{uf: forest;
@@ -189,10 +227,10 @@ type state =
mutable diseq: disequality list;
mutable quant: quant_eq list;
mutable pa_classes: Intset.t;
- q_history: (identifier,int array) Hashtbl.t;
+ q_history: (int array) Identhash.t;
mutable rew_depth:int;
mutable changed:bool;
- by_type: (types,Intset.t) Hashtbl.t;
+ by_type: Intset.t Typehash.t;
mutable gls:Proof_type.goal Tacmach.sigma}
let dummy_node =
@@ -207,8 +245,8 @@ let empty depth gls:state =
size=0;
map=Array.create init_size dummy_node;
epsilons=[];
- axioms=Hashtbl.create init_size;
- syms=Hashtbl.create init_size};
+ axioms=Constrhash.create init_size;
+ syms=Termhash.create init_size};
terms=Intset.empty;
combine=Queue.create ();
marks=Queue.create ();
@@ -216,9 +254,9 @@ let empty depth gls:state =
diseq=[];
quant=[];
pa_classes=Intset.empty;
- q_history=Hashtbl.create init_size;
+ q_history=Identhash.create init_size;
rew_depth=depth;
- by_type=Hashtbl.create init_size;
+ by_type=Constrhash.create init_size;
changed=false;
gls=gls}
@@ -384,7 +422,7 @@ let pr_term t = str "[" ++
let rec add_term state t=
let uf=state.uf in
- try Hashtbl.find uf.syms t with
+ try Termhash.find uf.syms t with
Not_found ->
let b=next uf in
let typ = pf_type_of state.gls (constr_of_term t) in
@@ -430,10 +468,10 @@ let rec add_term state t=
term=t}
in
uf.map.(b)<-new_node;
- Hashtbl.add uf.syms t b;
- Hashtbl.replace state.by_type typ
+ Termhash.add uf.syms t b;
+ Typehash.replace state.by_type typ
(Intset.add b
- (try Hashtbl.find state.by_type typ with
+ (try Typehash.find state.by_type typ with
Not_found -> Intset.empty));
b
@@ -441,7 +479,7 @@ let add_equality state c s t=
let i = add_term state s in
let j = add_term state t in
Queue.add {lhs=i;rhs=j;rule=Axiom(c,false)} state.combine;
- Hashtbl.add state.uf.axioms c (s,t)
+ Constrhash.add state.uf.axioms c (s,t)
let add_disequality state from s t =
let i = add_term state s in
@@ -461,7 +499,7 @@ let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) =
let is_redundant state id args =
try
let norm_args = Array.map (find state.uf) args in
- let prev_args = Hashtbl.find_all state.q_history id in
+ let prev_args = Identhash.find_all state.q_history id in
List.exists
(fun old_args ->
Util.array_for_all2 (fun i j -> i = find state.uf j)
@@ -476,7 +514,7 @@ let add_inst state (inst,int_subst) =
debug msgnl (str "discarding redundant (dis)equality")
else
begin
- Hashtbl.add state.q_history inst.qe_hyp_id int_subst;
+ Identhash.add state.q_history inst.qe_hyp_id int_subst;
let subst = build_subst (forest state) int_subst in
let prfhead= mkVar inst.qe_hyp_id in
let args = Array.map constr_of_term subst in
@@ -532,9 +570,9 @@ let union state i1 i2 eq=
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
link state.uf i1 i2 eq;
- Hashtbl.replace state.by_type r1.class_type
+ Constrhash.replace state.by_type r1.class_type
(Intset.remove i1
- (try Hashtbl.find state.by_type r1.class_type with
+ (try Constrhash.find state.by_type r1.class_type with
Not_found -> Intset.empty));
let f= Intset.union r1.fathers r2.fathers in
r2.weight<-Intset.cardinal f;
@@ -691,11 +729,11 @@ let __eps__ = id_of_string "_eps_"
let new_state_var typ state =
let id = pf_get_new_id __eps__ state.gls in
- state.gls<-
- {state.gls with it =
- {state.gls.it with evar_hyps =
- Environ.push_named_context_val (id,None,typ)
- state.gls.it.evar_hyps}};
+ let {it=gl ; sigma=sigma} = state.gls in
+ let new_hyps =
+ Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in
+ let gls = Goal.V82.new_goal_with sigma gl new_hyps in
+ state.gls<- gls;
id
let complete_one_class state i=
@@ -763,14 +801,14 @@ let rec do_match state res pb_stack =
else (* mismatch for non-linear variable in pattern *) ()
| PApp (f,[]) ->
begin
- try let j=Hashtbl.find uf.syms f in
+ try let j=Termhash.find uf.syms f in
if find uf j =cl then
Stack.push {mp with mp_stack=remains} pb_stack
with Not_found -> ()
end
| PApp(f, ((last_arg::rem_args) as args)) ->
try
- let j=Hashtbl.find uf.syms f in
+ let j=Termhash.find uf.syms f in
let paf={fsym=j;fnargs=List.length args} in
let rep=get_representative uf cl in
let good_terms = PafMap.find paf rep.functions in
@@ -788,7 +826,7 @@ let rec do_match state res pb_stack =
let paf_of_patt syms = function
PVar _ -> invalid_arg "paf_of_patt: pattern is trivial"
| PApp (f,args) ->
- {fsym=Hashtbl.find syms f;
+ {fsym=Termhash.find syms f;
fnargs=List.length args}
let init_pb_stack state =
@@ -810,7 +848,7 @@ let init_pb_stack state =
| Trivial typ ->
begin
try
- Hashtbl.find state.by_type typ
+ Typehash.find state.by_type typ
with Not_found -> Intset.empty
end in
Intset.iter (fun i ->
@@ -833,7 +871,7 @@ let init_pb_stack state =
| Trivial typ ->
begin
try
- Hashtbl.find state.by_type typ
+ Typehash.find state.by_type typ
with Not_found -> Intset.empty
end in
Intset.iter (fun i ->
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 8786c907..78dbee3f 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Term
open Names
@@ -24,6 +22,8 @@ type term =
| Appli of term*term
| Constructor of cinfo (* constructor arity + nhyps *)
+val term_equal : term -> term -> bool
+
type patt_kind =
Normal
| Trivial of types
@@ -66,13 +66,16 @@ type explanation =
| Contradiction of disequality
| Incomplete
+module Constrhash : Hashtbl.S with type key = constr
+module Termhash : Hashtbl.S with type key = term
+
val constr_of_term : term -> constr
val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
val forest : state -> forest
-val axioms : forest -> (constr, term * term) Hashtbl.t
+val axioms : forest -> (term * term) Constrhash.t
val epsilons : forest -> pa_constructor list
@@ -127,7 +130,7 @@ val do_match : state ->
val init_pb_stack : state -> matching_problem Stack.t
-val paf_of_patt : (term, int) Hashtbl.t -> ccpattern -> pa_fun
+val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun
val find_instances : state -> (quant_eq * int array) list
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 6981c5a0..bb1d50c9 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccproof.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
@@ -45,7 +43,7 @@ let rec ptrans p1 p3=
| Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
| _, _ ->
- if p1.p_rhs = p3.p_lhs then
+ if term_equal p1.p_rhs p3.p_lhs then
{p_lhs=p1.p_lhs;
p_rhs=p3.p_rhs;
p_rule=Trans (p1,p3)}
@@ -70,13 +68,13 @@ let rec psym p =
| Congr (p1,p2)-> pcongr (psym p1) (psym p2)
let pax axioms s =
- let l,r = Hashtbl.find axioms s in
+ let l,r = Constrhash.find axioms s in
{p_lhs=l;
p_rhs=r;
p_rule=Ax s}
let psymax axioms s =
- let l,r = Hashtbl.find axioms s in
+ let l,r = Constrhash.find axioms s in
{p_lhs=r;
p_rhs=l;
p_rule=SymAx s}
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index a58637f9..67819596 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccproof.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Ccalgo
open Names
open Term
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5b477b4d..ec31f891 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-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: cctac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* This file is the interface between the c-c algorithm and Coq *)
open Evd
@@ -20,7 +18,6 @@ open Nameops
open Inductiveops
open Declarations
open Term
-open Termops
open Tacmach
open Tactics
open Tacticals
@@ -66,8 +63,8 @@ let rec decompose_term env sigma t=
let tf=decompose_term env sigma f in
let targs=Array.map (decompose_term env sigma) args in
Array.fold_left (fun s t->Appli (s,t)) tf targs
- | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
- let b = pop _b in
+ | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+ let b = Termops.pop _b in
let sort_b = sf_of env sigma b in
let sort_a = sf_of env sigma a in
Appli(Appli(Product (sort_a,sort_b) ,
@@ -113,8 +110,8 @@ let rec pattern_of_constr env sigma c =
(array_map_to_list (pattern_of_constr env sigma) args) in
PApp (pf,List.rev pargs),
List.fold_left Intset.union Intset.empty lrels
- | Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
- let b =pop _b in
+ | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
+ let b = Termops.pop _b in
let pa,sa = pattern_of_constr env sigma a in
let pb,sb = pattern_of_constr env sigma b in
let sort_b = sf_of env sigma b in
@@ -214,9 +211,9 @@ let rec make_prb gls depth additionnal_terms =
neg_hyps:=(cid,nh):: !neg_hyps
| `Rule patts -> add_quant state id true patts
| `Nrule patts -> add_quant state id false patts
- end) (Environ.named_context_of_val gls.it.evar_hyps);
+ end) (Environ.named_context_of_val (Goal.V82.hyps gls.sigma gls.it));
begin
- match atom_of_constr env sigma gls.it.evar_concl with
+ match atom_of_constr env sigma (pf_concl gls) with
`Eq (t,a,b) -> add_disequality state Goal a b
| `Other g ->
List.iter
@@ -260,19 +257,19 @@ let rec proof_tac p gls =
| SymAx c ->
let l=constr_of_term p.p_lhs and
r=constr_of_term p.p_rhs in
- let typ = refresh_universes (pf_type_of gls l) in
+ let typ = Termops.refresh_universes (pf_type_of gls l) in
exact_check
(mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
| Refl t ->
let lr = constr_of_term t in
- let typ = refresh_universes (pf_type_of gls lr) in
+ let typ = Termops.refresh_universes (pf_type_of gls lr) in
exact_check
(mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls
| Trans (p1,p2)->
let t1 = constr_of_term p1.p_lhs and
t2 = constr_of_term p1.p_rhs and
t3 = constr_of_term p2.p_rhs in
- let typ = refresh_universes (pf_type_of gls t2) in
+ let typ = Termops.refresh_universes (pf_type_of gls t2) in
let prf =
mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in
tclTHENS (refine prf) [(proof_tac p1);(proof_tac p2)] gls
@@ -281,9 +278,9 @@ let rec proof_tac p gls =
and tx1=constr_of_term p2.p_lhs
and tf2=constr_of_term p1.p_rhs
and tx2=constr_of_term p2.p_rhs in
- let typf = refresh_universes (pf_type_of gls tf1) in
- let typx = refresh_universes (pf_type_of gls tx1) in
- let typfx = refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
+ let typf = Termops.refresh_universes (pf_type_of gls tf1) in
+ let typx = Termops.refresh_universes (pf_type_of gls tx1) in
+ let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
let id = pf_get_new_id (id_of_string "f") gls in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 =
@@ -311,8 +308,8 @@ let rec proof_tac p gls =
let ti=constr_of_term prf.p_lhs in
let tj=constr_of_term prf.p_rhs in
let default=constr_of_term p.p_lhs in
- let intype=refresh_universes (pf_type_of gls ti) in
- let outtype=refresh_universes (pf_type_of gls default) in
+ let intype = Termops.refresh_universes (pf_type_of gls ti) in
+ let outtype = Termops.refresh_universes (pf_type_of gls default) in
let special=mkRel (1+nargs-argind) in
let proj=build_projection intype outtype cstr special default gls in
let injt=
@@ -321,7 +318,7 @@ let rec proof_tac p gls =
let refute_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let intype=refresh_universes (pf_type_of gls tt1) in
+ let intype = Termops.refresh_universes (pf_type_of gls tt1) in
let neweq=
mkApp(Lazy.force _eq,
[|intype;tt1;tt2|]) in
@@ -332,7 +329,7 @@ let refute_tac c t1 t2 p gls =
let convert_to_goal_tac c t1 t2 p gls =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let sort=refresh_universes (pf_type_of gls tt2) in
+ let sort = Termops.refresh_universes (pf_type_of gls tt2) in
let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
let e=pf_get_new_id (id_of_string "e") gls in
let x=pf_get_new_id (id_of_string "X") gls in
@@ -352,14 +349,14 @@ let convert_to_hyp_tac c1 t1 c2 t2 p gls =
let discriminate_tac cstr p gls =
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
- let intype=refresh_universes (pf_type_of gls t1) in
+ let intype = Termops.refresh_universes (pf_type_of gls t1) in
let concl=pf_concl gls in
- let outsort=mkType (new_univ ()) in
+ let outsort = mkType (Termops.new_univ ()) in
let xid=pf_get_new_id (id_of_string "X") gls in
let tid=pf_get_new_id (id_of_string "t") gls in
let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
let trivial=pf_type_of gls identity in
- let outtype=mkType (new_univ ()) in
+ let outtype = mkType (Termops.new_univ ()) in
let pred=mkLambda(Name xid,outtype,mkRel 1) in
let hid=pf_get_new_id (id_of_string "Heq") gls in
let proj=build_projection intype outtype cstr trivial concl gls in
@@ -414,7 +411,7 @@ let cc_tactic depth additionnal_terms gls=
str "\"congruence with (" ++
prlist_with_sep
(fun () -> str ")" ++ pr_spc () ++ str "(")
- (print_constr_env (pf_env gls))
+ (Termops.print_constr_env (pf_env gls))
terms_to_complete ++
str ")\","
end);
@@ -456,7 +453,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
let f_equal gl =
let cut_eq c1 c2 =
- let ty = refresh_universes (pf_type_of gl c1) in
+ let ty = Termops.refresh_universes (pf_type_of gl c1) in
tclTHENTRY
(Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
(simple_reflexivity ())
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index b3d5c16b..32f56163 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cctac.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Term
open Proof_type
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index eb58c5eb..881b9bee 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-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,6 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_congruence.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Cctac
open Tactics
open Tacticals
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 03:36:23 +0000