Imported Upstream version 8.5~beta1+dfsg

8 files changed, 747 insertions, 547 deletions

diff --git a/plugins/cc/README b/plugins/cc/README
index 073b140e..c616b5da 100644
--- a/plugins/cc/README
+++ b/plugins/cc/README
@@ -3,7 +3,7 @@ cctac: congruence-closure for coq
 
 author: Pierre Corbineau, 
 	Stage de DEA au LSV, ENS Cachan
-	Thèse au LRI, Université Paris Sud XI 
+	Thèse au LRI, Université Paris Sud XI 
 
 Files :
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 056ae3a9..29bca862 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,22 +8,24 @@
 
 (* This file implements the basic congruence-closure algorithm by *)
 (* Downey,Sethi and Tarjan. *)
+(* Plus some e-matching and constructor handling by P. Corbineau *)
 
+open Errors
 open Util
 open Pp
 open Goptions
 open Names
 open Term
+open Vars
 open Tacmach
 open Evd
-open Proof_type
 
 let init_size=5
 
 let cc_verbose=ref false
 
-let debug f x =
-  if !cc_verbose then f x
+let debug x =
+  if !cc_verbose then msg_debug x
 
 let _=
   let gdopt=
@@ -42,32 +44,39 @@ module ST=struct
 
   (* l: sign -> term r: term -> sign *)
 
-  type t = {toterm:(int*int,int) Hashtbl.t;
-	    tosign:(int,int*int) Hashtbl.t}
+  module IntTable = Hashtbl.Make(Int)
+  module IntPair =
+  struct
+    type t = int * int
+    let equal (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2
+    let hash (i, j) = Hashset.Combine.combine (Int.hash i) (Int.hash j)
+  end
+  module IntPairTable = Hashtbl.Make(IntPair)
+
+  type t = {toterm: int IntPairTable.t;
+	    tosign: (int * int) IntTable.t}
 
   let empty ()=
-    {toterm=Hashtbl.create init_size;
-     tosign=Hashtbl.create init_size}
+    {toterm=IntPairTable.create init_size;
+     tosign=IntTable.create init_size}
 
   let enter t sign st=
-    if Hashtbl.mem st.toterm sign then
-	anomaly "enter: signature already entered"
+    if IntPairTable.mem st.toterm sign then
+	anomaly ~label:"enter" (Pp.str "signature already entered")
     else
-	Hashtbl.replace st.toterm sign t;
-	Hashtbl.replace st.tosign t sign
-
-  let query sign st=Hashtbl.find st.toterm sign
+	IntPairTable.replace st.toterm sign t;
+	IntTable.replace st.tosign t sign
 
-  let rev_query term st=Hashtbl.find st.tosign term
+  let query sign st=IntPairTable.find st.toterm sign
 
   let delete st t=
-    try let sign=Hashtbl.find st.tosign t in
-	Hashtbl.remove st.toterm sign;
-	Hashtbl.remove st.tosign t
+    try let sign=IntTable.find st.tosign t in
+	IntPairTable.remove st.toterm sign;
+	IntTable.remove st.tosign t
     with
 	Not_found -> ()
 
-  let rec delete_set st s = Intset.iter (delete st) s
+  let delete_set st s = Int.Set.iter (delete st) s
 
 end
 
@@ -84,45 +93,78 @@ type pa_mark=
     Fmark of pa_fun
   | Cmark of pa_constructor
 
-module PacMap=Map.Make(struct
-			 type t=pa_constructor
-			 let compare=Pervasives.compare end)
+module PacOrd =
+struct
+  type t = pa_constructor
+  let compare { cnode = cnode0; arity = arity0; args = args0 }
+              { cnode = cnode1; arity = arity1; args = args1 } =
+    let cmp = Int.compare cnode0 cnode1 in
+    if cmp = 0 then
+      let cmp' = Int.compare arity0 arity1 in
+      if cmp' = 0 then
+        List.compare Int.compare args0 args1
+      else
+        cmp'
+    else
+      cmp
+end
+
+module PafOrd =
+struct
+  type t = pa_fun
+  let compare { fsym = fsym0; fnargs = fnargs0 } { fsym = fsym1; fnargs = fnargs1 } =
+    let cmp = Int.compare fsym0 fsym1 in
+    if cmp = 0 then
+      Int.compare fnargs0 fnargs1
+    else
+      cmp
+end
 
-module PafMap=Map.Make(struct
-			 type t=pa_fun
-			 let compare=Pervasives.compare end)
+module PacMap=Map.Make(PacOrd)
+module PafMap=Map.Make(PafOrd)
 
 type cinfo=
-    {ci_constr: constructor; (* inductive type *)
+    {ci_constr: pconstructor; (* inductive type *)
      ci_arity: int;     (* # args *)
      ci_nhyps: int}     (* # projectable args *)
 
+let family_eq f1 f2 = match f1, f2 with
+| InProp, InProp
+| InSet, InSet
+| InType, InType -> true
+| _ -> false
+
 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 *)
 
 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
+    | Symb c1, Symb c2 -> eq_constr_nounivs c1 c2
+    | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2
+    | Eps i1, Eps i2 -> Id.equal i1 i2
     | 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
+    | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1},
+      Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} ->
+      Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *)
+    | _ -> false
+
+open Hashset.Combine
 
-open Hashtbl_alt.Combine
+let hash_sorts_family = function
+| InProp -> 0
+| InSet -> 1
+| InType -> 2
 
 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)
+  | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2)
+  | Eps i -> combine 3 (Id.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
+  | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
 
 type ccpattern =
     PApp of term * ccpattern list (* arguments are reversed *)
@@ -151,14 +193,16 @@ type patt_kind =
   | Creates_variables
 
 type quant_eq =
-    {qe_hyp_id: identifier;
-     qe_pol: bool;
-     qe_nvars:int;
-     qe_lhs: ccpattern;
-     qe_lhs_valid:patt_kind;
-     qe_rhs: ccpattern;
-     qe_rhs_valid:patt_kind}
-
+  {
+    qe_hyp_id: Id.t;
+    qe_pol: bool;
+    qe_nvars:int;
+    qe_lhs: ccpattern;
+    qe_lhs_valid:patt_kind;
+    qe_rhs: ccpattern;
+    qe_rhs_valid:patt_kind
+  }
+    
 let swap eq : equality =
   let swap_rule=match eq.rule with
       Congruence -> Congruence
@@ -174,12 +218,11 @@ type inductive_status =
 
 type representative=
     {mutable weight:int;
-     mutable lfathers:Intset.t;
-     mutable fathers:Intset.t;
+     mutable lfathers:Int.Set.t;
+     mutable fathers:Int.Set.t;
      mutable inductive_status: inductive_status;
      class_type : Term.types;
-     mutable functions: Intset.t PafMap.t;
-     mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *)
+     mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
 
 type cl = Rep of representative| Eqto of int*equality
 
@@ -188,12 +231,13 @@ type vertex = Leaf| Node of (int*int)
 type node =
     {mutable clas:cl;
      mutable cpath: int;
+     mutable constructors: int PacMap.t;
      vertex:vertex;
      term:term}
 
 module Constrhash = Hashtbl.Make
   (struct type t = constr
-	  let equal = eq_constr
+	  let equal = eq_constr_nounivs
 	  let hash = hash_constr
    end)
 module Typehash = Constrhash
@@ -205,9 +249,9 @@ module Termhash = Hashtbl.Make
    end)
 
 module Identhash = Hashtbl.Make
-  (struct type t = identifier
-	  let equal = Pervasives.(=)
-	  let hash = Hashtbl.hash
+  (struct type t = Id.t
+	  let equal = Id.equal
+	  let hash = Id.hash
    end)
 
 type forest=
@@ -221,45 +265,54 @@ type forest=
 type state =
     {uf: forest;
      sigtable:ST.t;
-     mutable terms: Intset.t;
+     mutable terms: Int.Set.t;
      combine: equality Queue.t;
      marks: (int * pa_mark) Queue.t;
      mutable diseq: disequality list;
      mutable quant: quant_eq list;
-     mutable pa_classes: Intset.t;
+     mutable pa_classes: Int.Set.t;
      q_history: (int array) Identhash.t;
      mutable rew_depth:int;
      mutable changed:bool;
-     by_type: Intset.t Typehash.t;
+     by_type: Int.Set.t Typehash.t;
      mutable gls:Proof_type.goal Tacmach.sigma}
 
 let dummy_node =
-  {clas=Eqto(min_int,{lhs=min_int;rhs=min_int;rule=Congruence});
-   cpath=min_int;
-   vertex=Leaf;
-   term=Symb (mkRel min_int)}
-
+  {
+    clas=Eqto (min_int,{lhs=min_int;rhs=min_int;rule=Congruence});
+    cpath=min_int;
+    constructors=PacMap.empty;
+    vertex=Leaf;
+    term=Symb (mkRel min_int)
+  }
+
+let empty_forest() =
+  {
+    max_size=init_size;
+    size=0;
+    map=Array.make init_size dummy_node;
+    epsilons=[];
+    axioms=Constrhash.create init_size;
+    syms=Termhash.create init_size
+  }
+    
 let empty depth gls:state =
-  {uf=
-     {max_size=init_size;
-      size=0;
-      map=Array.create init_size dummy_node;
-      epsilons=[];
-      axioms=Constrhash.create init_size;
-      syms=Termhash.create init_size};
-  terms=Intset.empty;
-  combine=Queue.create ();
-  marks=Queue.create ();
-  sigtable=ST.empty ();
-  diseq=[];
-  quant=[];
-  pa_classes=Intset.empty;
-  q_history=Identhash.create init_size;
-  rew_depth=depth;
-  by_type=Constrhash.create init_size;
-  changed=false;
-  gls=gls}
-
+  {
+    uf= empty_forest ();
+    terms=Int.Set.empty;
+    combine=Queue.create ();
+    marks=Queue.create ();
+    sigtable=ST.empty ();
+    diseq=[];
+    quant=[];
+    pa_classes=Int.Set.empty;
+    q_history=Identhash.create init_size;
+    rew_depth=depth;
+    by_type=Constrhash.create init_size;
+    changed=false;
+    gls=gls
+  }
+    
 let forest state = state.uf
 
 let compress_path uf i j = uf.map.(j).cpath<-i
@@ -274,15 +327,25 @@ let find uf i= find_aux uf [] i
 let get_representative uf i=
   match uf.map.(i).clas with
       Rep r -> r
-    | _ -> anomaly "get_representative: not a representative"
+    | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative")
+
+let get_constructors uf i= uf.map.(i).constructors
 
 let find_pac uf i pac =
-  PacMap.find pac (get_representative uf i).constructors
+  PacMap.find pac (get_constructors uf i)
+
+let rec find_oldest_pac uf i pac=
+  try PacMap.find pac (get_constructors uf i) with
+    Not_found -> 
+      match uf.map.(i).clas with 
+	Eqto (j,_) -> find_oldest_pac uf j pac
+      | Rep _ -> raise Not_found
+     
 
 let get_constructor_info uf i=
   match uf.map.(i).term with
       Constructor cinfo->cinfo
-    | _ -> anomaly "get_constructor: not a constructor"
+    | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor")
 
 let size uf i=
   (get_representative uf i).weight
@@ -294,13 +357,13 @@ let epsilons uf = uf.epsilons
 let add_lfather uf i t=
   let r=get_representative uf i in
     r.weight<-r.weight+1;
-    r.lfathers<-Intset.add t r.lfathers;
-    r.fathers <-Intset.add t r.fathers
+    r.lfathers<-Int.Set.add t r.lfathers;
+    r.fathers <-Int.Set.add t r.fathers
 
 let add_rfather uf i t=
   let r=get_representative uf i in
     r.weight<-r.weight+1;
-    r.fathers <-Intset.add t r.fathers
+    r.fathers <-Int.Set.add t r.fathers
 
 exception Discriminable of int * pa_constructor * int * pa_constructor
 
@@ -313,21 +376,21 @@ let tail_pac p=
 let fsucc paf =
   {paf with fnargs=succ paf.fnargs}
 
-let add_pac rep pac t =
-  if not (PacMap.mem pac rep.constructors) then
-    rep.constructors<-PacMap.add pac t rep.constructors
+let add_pac node pac t =
+  if not (PacMap.mem pac node.constructors) then
+    node.constructors<-PacMap.add pac t node.constructors
 
 let add_paf rep paf t =
   let already =
-    try PafMap.find paf rep.functions with Not_found -> Intset.empty in
-    rep.functions<- PafMap.add paf (Intset.add t already) rep.functions
+    try PafMap.find paf rep.functions with Not_found -> Int.Set.empty in
+    rep.functions<- PafMap.add paf (Int.Set.add t already) rep.functions
 
 let term uf i=uf.map.(i).term
 
 let subterms uf i=
   match uf.map.(i).vertex with
       Node(j,k) -> (j,k)
-    | _ -> anomaly "subterms: not a node"
+    | _ -> anomaly ~label:"subterms" (Pp.str "not a node")
 
 let signature uf i=
   let j,k=subterms uf i in (find uf j,find uf k)
@@ -335,9 +398,9 @@ let signature uf i=
 let next uf=
   let size=uf.size in
   let nsize= succ size in
-    if nsize=uf.max_size then
+    if Int.equal nsize uf.max_size then
       let newmax=uf.max_size * 3 / 2 + 1 in
-      let newmap=Array.create newmax dummy_node in
+      let newmap=Array.make newmax dummy_node in
 	begin
 	  uf.max_size<-newmax;
 	  Array.blit uf.map 0 newmap 0 size;
@@ -349,46 +412,63 @@ let next uf=
 
 let new_representative typ =
   {weight=0;
-   lfathers=Intset.empty;
-   fathers=Intset.empty;
+   lfathers=Int.Set.empty;
+   fathers=Int.Set.empty;
    inductive_status=Unknown;
    class_type=typ;
-   functions=PafMap.empty;
-   constructors=PacMap.empty}
+   functions=PafMap.empty}
 
 (* rebuild a constr from an applicative term *)
 
-let _A_ = Name (id_of_string "A")
-let _B_ = Name (id_of_string "A")
+let _A_ = Name (Id.of_string "A")
+let _B_ = Name (Id.of_string "A")
 let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
 
 let cc_product s1 s2 =
-  mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
-	   mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
+  mkLambda(_A_,mkSort(Universes.new_sort_in_family s1),
+	   mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_))
 
 let rec constr_of_term = function
-    Symb s->s
+    Symb s-> applist_projection s []
   | Product(s1,s2) -> cc_product s1 s2
   | Eps id -> mkVar id
-  | Constructor cinfo -> mkConstruct cinfo.ci_constr
+  | Constructor cinfo -> mkConstructU cinfo.ci_constr
   | Appli (s1,s2)->
       make_app [(constr_of_term s2)] s1
 and make_app l=function
     Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
-  | other -> applistc (constr_of_term other) l
+  | other -> 
+    applist_proj other l
+and applist_proj c l =
+  match c with
+  | Symb s -> applist_projection s l
+  | _ -> applistc (constr_of_term c) l
+and applist_projection c l =
+  match kind_of_term c with
+  | Const c when Environ.is_projection (fst c) (Global.env()) ->
+    let p = Projection.make (fst c) false in
+    (match l with 
+    | [] -> (* Expand the projection *)
+      let ty,_ = Typeops.type_of_constant (Global.env ()) c in
+      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
+    | hd :: tl ->
+      applistc (mkProj (p, hd)) tl)
+  | _ -> applistc c l
 
 let rec canonize_name c =
   let func =  canonize_name in
     match kind_of_term c with
-      | Const kn ->
+      | Const (kn,u) ->
 	  let canon_const = constant_of_kn (canonical_con kn) in 
-	    (mkConst canon_const)
-      | Ind (kn,i) ->
+	    (mkConstU (canon_const,u))
+      | Ind ((kn,i),u) ->
 	  let canon_mind = mind_of_kn (canonical_mind kn) in
-	    (mkInd (canon_mind,i))
-      | Construct ((kn,i),j) ->
+	    (mkIndU ((canon_mind,i),u))
+      | Construct (((kn,i),j),u) ->
 	  let canon_mind = mind_of_kn (canonical_mind kn) in
-	    mkConstruct ((canon_mind,i),j) 
+	    mkConstructU (((canon_mind,i),j),u)
       | Prod (na,t,ct) ->
 	  mkProd (na,func t, func ct)
       | Lambda (na,t,ct) ->
@@ -396,16 +476,22 @@ let rec canonize_name c =
       | LetIn (na,b,t,ct) ->
 	  mkLetIn (na, func b,func t,func ct)
       | App (ct,l) ->
-	  mkApp (func ct,array_smartmap func l)
+	  mkApp (func ct,Array.smartmap func l)
+      | Proj(p,c) ->
+	let p' = Projection.map (fun kn ->
+          constant_of_kn (canonical_con kn)) p in 
+	  (mkProj (p', func c))
       | _ -> c
 
 (* rebuild a term from a pattern and a substitution *)
 
 let build_subst uf subst =
-  Array.map (fun i ->
-	       try term uf i
-	       with e when Errors.noncritical e ->
-                 anomaly "incomplete matching") subst
+  Array.map
+    (fun i ->
+      try term uf i
+      with e when Errors.noncritical e ->
+        anomaly (Pp.str "incomplete matching"))
+    subst
 
 let rec inst_pattern subst = function
     PVar i ->
@@ -415,8 +501,8 @@ let rec inst_pattern subst = function
 	(fun spat f -> Appli (f,inst_pattern subst spat))
 	   args t
 
-let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]"
+let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
+  Termops.print_constr (constr_of_term (term uf i)) ++ str "]"
 
 let pr_term t = str "[" ++
   Termops.print_constr (constr_of_term t) ++ str "]"
@@ -426,7 +512,8 @@ let rec add_term state t=
     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
+          let trm = constr_of_term t in
+	  let typ = pf_type_of state.gls trm in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -437,20 +524,23 @@ let rec add_term state t=
 		    Queue.add (b,Fmark paf) state.marks;
 		    {clas= Rep (new_representative typ);
 		     cpath= -1;
+		     constructors=PacMap.empty;
 		     vertex= Leaf;
 		     term= t}
 	      | Eps id ->
 		  {clas= Rep (new_representative typ);
 		   cpath= -1;
+		   constructors=PacMap.empty;
 		   vertex= Leaf;
 		   term= t}
 	      | Appli (t1,t2) ->
 		  let i1=add_term state t1 and i2=add_term state t2 in
 		    add_lfather uf (find uf i1) b;
 		    add_rfather uf (find uf i2) b;
-		    state.terms<-Intset.add b state.terms;
+		    state.terms<-Int.Set.add b state.terms;
 		    {clas= Rep (new_representative typ);
 		     cpath= -1;
+		     constructors=PacMap.empty;
 		     vertex= Node(i1,i2);
 		     term= t}
 	      | Constructor cinfo ->
@@ -465,15 +555,16 @@ let rec add_term state t=
 		    Queue.add (b,Cmark pac) state.marks;
 		    {clas=Rep (new_representative typ);
 		     cpath= -1;
+		     constructors=PacMap.empty;
 		     vertex=Leaf;
 		     term=t}
 	  in
 	    uf.map.(b)<-new_node;
 	    Termhash.add uf.syms t b;
 	    Typehash.replace state.by_type typ
-	      (Intset.add b
+	      (Int.Set.add b
 		 (try Typehash.find state.by_type typ with
-		      Not_found -> Intset.empty));
+		      Not_found -> Int.Set.empty));
 	    b
 
 let add_equality state c s t=
@@ -503,23 +594,23 @@ let is_redundant state id args =
     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)
+	 Util.Array.for_all2 (fun i j -> Int.equal i (find state.uf j))
          norm_args old_args)
       prev_args
     with Not_found -> false
 
 let add_inst state (inst,int_subst) =
-  check_for_interrupt ();
+  Control.check_for_interrupt ();
   if state.rew_depth > 0 then
   if is_redundant state inst.qe_hyp_id int_subst then
-    debug msgnl (str "discarding redundant (dis)equality")
+    debug (str "discarding redundant (dis)equality")
   else
     begin
       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
-      let _ = array_rev args in (* highest deBruijn index first *)
+      let _ = Array.rev args in (* highest deBruijn index first *)
       let prf= mkApp(prfhead,args) in
 	  let s = inst_pattern subst inst.qe_lhs
 	  and t = inst_pattern subst inst.qe_rhs in
@@ -527,20 +618,18 @@ let add_inst state (inst,int_subst) =
 	    state.rew_depth<-pred state.rew_depth;
 	    if inst.qe_pol then
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new equality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
 	    else
 	      begin
-		debug (fun () ->
-		  msgnl
-		   (str "Adding new disequality, depth="++ int state.rew_depth);
-	          msgnl (str "  [" ++ Termops.print_constr prf ++ str " : " ++
-			   pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
+		debug (
+		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
+	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
   end
@@ -552,75 +641,77 @@ let link uf i j eq = (* links i -> j *)
 
 let rec down_path uf i l=
   match uf.map.(i).clas with
-      Eqto(j,t)->down_path uf j (((i,j),t)::l)
+      Eqto (j,eq) ->down_path uf j (((i,j),eq)::l)
     | Rep _ ->l
 
+let eq_pair (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2
+
 let rec min_path=function
     ([],l2)->([],l2)
   | (l1,[])->(l1,[])
-  | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2)
+  | (((c1,t1)::q1),((c2,t2)::q2)) when eq_pair c1 c2 -> min_path (q1,q2)
   | cpl -> cpl
 
 let join_path uf i j=
-  assert (find uf i=find uf j);
+  assert (Int.equal (find uf i) (find uf j));
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
-  debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
-		 str " and " ++ pr_idx_term state i2 ++ str ".")) ();
+  debug (str "Linking " ++ pr_idx_term state.uf i1 ++
+		 str " and " ++ pr_idx_term state.uf i2 ++ str ".");
   let r1= get_representative state.uf i1
   and r2= get_representative state.uf i2 in
     link state.uf i1 i2 eq;
     Constrhash.replace state.by_type r1.class_type
-      (Intset.remove i1
+      (Int.Set.remove i1
 	 (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;
+	      Not_found -> Int.Set.empty));
+    let f= Int.Set.union r1.fathers r2.fathers in
+      r2.weight<-Int.Set.cardinal f;
       r2.fathers<-f;
-      r2.lfathers<-Intset.union r1.lfathers r2.lfathers;
+      r2.lfathers<-Int.Set.union r1.lfathers r2.lfathers;
       ST.delete_set state.sigtable r1.fathers;
-      state.terms<-Intset.union state.terms r1.fathers;
+      state.terms<-Int.Set.union state.terms r1.fathers;
       PacMap.iter
 	(fun pac b -> Queue.add (b,Cmark pac) state.marks)
-	r1.constructors;
+	state.uf.map.(i1).constructors;
       PafMap.iter
-	(fun paf -> Intset.iter
+	(fun paf -> Int.Set.iter
 	   (fun b -> Queue.add (b,Fmark paf) state.marks))
 	r1.functions;
       match r1.inductive_status,r2.inductive_status with
 	  Unknown,_ -> ()
 	| Partial pac,Unknown ->
 	    r2.inductive_status<-Partial pac;
-	    state.pa_classes<-Intset.remove i1 state.pa_classes;
-	    state.pa_classes<-Intset.add i2 state.pa_classes
+	    state.pa_classes<-Int.Set.remove i1 state.pa_classes;
+	    state.pa_classes<-Int.Set.add i2 state.pa_classes
 	| Partial _ ,(Partial _ |Partial_applied) ->
-	    state.pa_classes<-Intset.remove i1 state.pa_classes
+	    state.pa_classes<-Int.Set.remove i1 state.pa_classes
 	| Partial_applied,Unknown ->
 	    r2.inductive_status<-Partial_applied
 	| Partial_applied,Partial _ ->
-	    state.pa_classes<-Intset.remove i2 state.pa_classes;
+	    state.pa_classes<-Int.Set.remove i2 state.pa_classes;
 	    r2.inductive_status<-Partial_applied
 	| Total cpl,Unknown -> r2.inductive_status<-Total cpl;
 	| Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks
 	| _,_ -> ()
 
 let merge eq state = (* merge and no-merge *)
-  debug (fun () -> msgnl
-    (str "Merging " ++ pr_idx_term state eq.lhs ++
-       str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
+  debug
+    (str "Merging " ++ pr_idx_term state.uf eq.lhs ++
+       str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
   let uf=state.uf in
   let i=find uf eq.lhs
   and j=find uf eq.rhs in
-    if i<>j then
+    if not (Int.equal i j) then
       if (size uf i)<(size uf j) then
 	union state i j eq
       else
 	union state j i (swap eq)
 
 let update t state = (* update 1 and 2 *)
-  debug (fun () -> msgnl
-    (str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
   let (i,j) as sign = signature state.uf t in
   let (u,v) = subterms state.uf t in
   let rep = get_representative state.uf i in
@@ -628,12 +719,12 @@ let update t state = (* update 1 and 2 *)
       match rep.inductive_status with
 	  Partial _ ->
 	    rep.inductive_status <- Partial_applied;
-	    state.pa_classes <- Intset.remove i state.pa_classes
+	    state.pa_classes <- Int.Set.remove i state.pa_classes
 	| _ -> ()
     end;
     PacMap.iter
       (fun pac _ -> Queue.add (t,Cmark (append_pac v pac)) state.marks)
-      rep.constructors;
+      (get_constructors state.uf i);
     PafMap.iter
       (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks)
       rep.functions;
@@ -645,12 +736,13 @@ let update t state = (* update 1 and 2 *)
 
 let process_function_mark t rep paf state  =
   add_paf rep paf t;
-  state.terms<-Intset.union rep.lfathers state.terms
+  state.terms<-Int.Set.union rep.lfathers state.terms
 
 let process_constructor_mark t i rep pac state =
-    match rep.inductive_status with
+     add_pac state.uf.map.(i) pac t;
+     match rep.inductive_status with
 	Total (s,opac) ->
-	  if pac.cnode <> opac.cnode then (* Conflict *)
+	  if not (Int.equal pac.cnode opac.cnode) then (* Conflict *)
 	    raise (Discriminable (s,opac,t,pac))
 	  else (* Match *)
 	    let cinfo = get_constructor_info state.uf pac.cnode in
@@ -662,26 +754,26 @@ let process_constructor_mark t i rep pac state =
 			{lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)}
 			state.combine;
 		      f (n-1) q1 q2
-		  | _-> anomaly
-		      "add_pacs : weird error in injection subterms merge"
+		  | _-> anomaly ~label:"add_pacs"
+		      (Pp.str "weird error in injection subterms merge")
 	    in f cinfo.ci_nhyps opac.args pac.args
       | Partial_applied | Partial _ ->
-	  add_pac rep pac t;
-	  state.terms<-Intset.union rep.lfathers state.terms
+(*	  add_pac state.uf.map.(i) pac t; *)
+	  state.terms<-Int.Set.union rep.lfathers state.terms
       | Unknown ->
-	  if pac.arity = 0 then
+	  if Int.equal pac.arity 0 then
 	    rep.inductive_status <- Total (t,pac)
 	  else
 	    begin
-	      add_pac rep pac t;
-	      state.terms<-Intset.union rep.lfathers state.terms;
+	     (* add_pac state.uf.map.(i) pac t; *)
+	      state.terms<-Int.Set.union rep.lfathers state.terms;
 	      rep.inductive_status <- Partial pac;
-	      state.pa_classes<- Intset.add i state.pa_classes
+	      state.pa_classes<- Int.Set.add i state.pa_classes
 	    end
 
 let process_mark t m state =
-  debug (fun () -> msgnl
-    (str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
+  debug
+    (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
   let i=find state.uf t in
   let rep=get_representative state.uf i in
     match m with
@@ -696,14 +788,15 @@ type explanation =
 let check_disequalities state =
   let uf=state.uf in
   let rec check_aux = function
-      dis::q ->
-	debug (fun () -> msg
-	(str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-	 pr_idx_term state dis.rhs ++ str " ... ")) ();
-	if find uf dis.lhs=find uf dis.rhs then
-	  begin debug msgnl (str "Yes");Some dis end
-	else
-	  begin debug msgnl (str "No");check_aux q end
+    | dis::q ->
+        let (info, ans) =
+          if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis)
+          else (str "No", check_aux q)
+        in
+        let _ = debug
+        (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+         pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
+        ans
     | [] -> None
   in
     check_aux state.diseq
@@ -720,13 +813,13 @@ let one_step state =
 	  true
       with Queue.Empty ->
 	try
-	  let t = Intset.choose state.terms in
-	    state.terms<-Intset.remove t state.terms;
+	  let t = Int.Set.choose state.terms in
+	    state.terms<-Int.Set.remove t state.terms;
 	    update t state;
 	    true
 	with Not_found -> false
 
-let __eps__ = id_of_string "_eps_"
+let __eps__ = Id.of_string "_eps_"
 
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
@@ -752,10 +845,10 @@ let complete_one_class state i=
 	let ct = app (term state.uf i) typ pac.arity in
 	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
-    | _ -> anomaly "wrong incomplete class"
+    | _ -> anomaly (Pp.str "wrong incomplete class")
 
 let complete state =
-  Intset.iter (complete_one_class state) state.pa_classes
+  Int.Set.iter (complete_one_class state) state.pa_classes
 
 type matching_problem =
 {mp_subst : int array;
@@ -773,14 +866,14 @@ let make_fun_table state =
 	       (fun paf _ ->
 		  let elem =
 		    try PafMap.find paf !funtab
-		    with Not_found -> Intset.empty in
-		    funtab:= PafMap.add paf (Intset.add i elem) !funtab)
+		    with Not_found -> Int.Set.empty in
+		    funtab:= PafMap.add paf (Int.Set.add i elem) !funtab)
 	       rep.functions
 	 | _ -> ()) state.uf.map;
     !funtab
 
 
-let rec do_match state res pb_stack =
+let do_match state res pb_stack =
   let mp=Stack.pop pb_stack in
     match mp.mp_stack with
 	[] ->
@@ -795,13 +888,13 @@ let rec do_match state res pb_stack =
 		      Stack.push {mp with mp_stack=remains} pb_stack
 		    end
 		  else
-		    if mp.mp_subst.(pred i) = cl then
+		    if Int.equal mp.mp_subst.(pred i) cl then
 		      Stack.push {mp with mp_stack=remains} pb_stack
 		    else (* mismatch for non-linear variable in pattern *) ()
 	      | PApp (f,[]) ->
 		  begin
 		    try let j=Termhash.find uf.syms f in
-		      if find uf j =cl then
+		      if Int.equal (find uf j) cl then
 			Stack.push {mp with mp_stack=remains} pb_stack
 		    with Not_found -> ()
 		  end
@@ -819,7 +912,7 @@ let rec do_match state res pb_stack =
 			     mp_stack=
 			      (PApp(f,rem_args),s) ::
 				(last_arg,t) :: remains} pb_stack in
-		      Intset.iter aux good_terms
+		      Int.Set.iter aux good_terms
 		  with Not_found -> ()
 
 let paf_of_patt syms = function
@@ -836,21 +929,21 @@ let init_pb_stack state =
     begin
       let good_classes =
 	match inst.qe_lhs_valid with
-	  Creates_variables -> Intset.empty
+	  Creates_variables -> Int.Set.empty
 	| Normal ->
 	    begin
 	      try
 		let paf= paf_of_patt syms inst.qe_lhs in
 		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end
 	| Trivial typ ->
 	    begin
 	      try
 		Typehash.find state.by_type typ
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end in
-	Intset.iter (fun i ->
+	Int.Set.iter (fun i ->
 		       Stack.push
 			 {mp_subst = Array.make inst.qe_nvars (-1);
 			  mp_inst=inst;
@@ -859,21 +952,21 @@ let init_pb_stack state =
     begin
       let good_classes =
 	match inst.qe_rhs_valid with
-	  Creates_variables -> Intset.empty
+	  Creates_variables -> Int.Set.empty
 	| Normal ->
 	    begin
 	      try
 		let paf= paf_of_patt syms inst.qe_rhs in
 		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end
 	| Trivial typ ->
 	    begin
 	      try
 		Typehash.find state.by_type typ
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end in
-	Intset.iter (fun i ->
+	Int.Set.iter (fun i ->
 		       Stack.push
 			 {mp_subst = Array.make inst.qe_nvars (-1);
 			  mp_inst=inst;
@@ -886,28 +979,28 @@ let find_instances state =
   let pb_stack= init_pb_stack state in
   let res =ref [] in
   let _ =
-    debug msgnl (str "Running E-matching algorithm ... ");
+    debug (str "Running E-matching algorithm ... ");
     try
       while true do
-	check_for_interrupt ();
+	Control.check_for_interrupt ();
 	do_match state res pb_stack
       done;
-      anomaly "get out of here !"
+      anomaly (Pp.str "get out of here !")
     with Stack.Empty -> () in
     !res
 
 let rec execute first_run state =
-  debug msgnl (str "Executing ... ");
+  debug (str "Executing ... ");
   try
     while
-      check_for_interrupt ();
+      Control.check_for_interrupt ();
       one_step state do ()
     done;
     match check_disequalities state with
 	None ->
-	  if not(Intset.is_empty state.pa_classes) then
+	  if not(Int.Set.is_empty state.pa_classes) then
 	    begin
-	      debug msgnl (str "First run was incomplete, completing ... ");
+	      debug (str "First run was incomplete, completing ... ");
 	      complete state;
 	      execute false state
 	    end
@@ -922,12 +1015,12 @@ let rec execute first_run state =
 		  end
 		else
 	      begin
-		debug msgnl (str "Out of instances ... ");
+		debug (str "Out of instances ... ");
 		None
 	      end
 	    else
 	      begin
-		debug msgnl (str "Out of depth ... ");
+		debug (str "Out of depth ... ");
 		None
 	      end
       | Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index e4713728..c72843d5 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,40 +10,39 @@ open Util
 open Term
 open Names
 
+type pa_constructor =
+    { cnode : int;
+      arity : int;
+      args  : int list}
+
+type pa_fun=
+    {fsym:int;
+     fnargs:int}
+
+
+module PafMap : Map.S with type key = pa_fun
+module PacMap : Map.S with type key = pa_constructor
+
 type cinfo =
-    {ci_constr: constructor; (* inductive type *)
+    {ci_constr: pconstructor; (* inductive type *)
      ci_arity: int;     (* # args *)
      ci_nhyps: int}     (* # projectable args *)
 
 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 *)
 
-val term_equal : term -> term -> bool
+module Constrhash : Hashtbl.S with type key = constr
+module Termhash : Hashtbl.S with type key = term
 
-type patt_kind =
-    Normal
-  | Trivial of types
-  | Creates_variables
 
 type ccpattern =
     PApp of term * ccpattern list
   | PVar of int
 
-type pa_constructor =
-    { cnode : int;
-      arity : int;
-      args  : int list}
-
-module PacMap : Map.S with type key = pa_constructor
-
-type forest
-
-type state
-
 type rule=
     Congruence
   | Axiom of constr * bool
@@ -61,17 +60,67 @@ type equality = rule eq
 
 type disequality = from eq
 
+type patt_kind =
+    Normal
+  | Trivial of types
+  | Creates_variables
+
+type quant_eq=
+    {qe_hyp_id: Id.t;
+     qe_pol: bool;
+     qe_nvars:int;
+     qe_lhs: ccpattern;
+     qe_lhs_valid:patt_kind;
+     qe_rhs: ccpattern;
+     qe_rhs_valid:patt_kind}
+
+type inductive_status =
+    Unknown
+  | Partial of pa_constructor
+  | Partial_applied
+  | Total of (int * pa_constructor)
+
+type representative=
+    {mutable weight:int;
+     mutable lfathers:Int.Set.t;
+     mutable fathers:Int.Set.t;
+     mutable inductive_status: inductive_status;
+     class_type : Term.types;
+     mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
+
+type cl = Rep of representative| Eqto of int*equality
+
+type vertex = Leaf| Node of (int*int)
+
+type node =
+    {mutable clas:cl;
+     mutable cpath: int;
+     mutable constructors: int PacMap.t;
+     vertex:vertex;
+     term:term}
+
+type forest=
+    {mutable max_size:int;
+     mutable size:int;
+     mutable map: node array;
+     axioms: (term*term) Constrhash.t;
+     mutable epsilons: pa_constructor list;
+     syms: int Termhash.t}
+
+type state
+
 type explanation =
     Discrimination of (int*pa_constructor*int*pa_constructor)
   | Contradiction of disequality
   | Incomplete
 
-module Constrhash : Hashtbl.S with type key = constr
-module Termhash : Hashtbl.S with type key = term
+type matching_problem
+
+val term_equal : term -> term -> bool
 
 val constr_of_term : term -> constr
 
-val debug : (Pp.std_ppcmds -> unit) -> Pp.std_ppcmds -> unit
+val debug : Pp.std_ppcmds -> unit
 
 val forest : state -> forest
 
@@ -87,7 +136,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
@@ -96,6 +145,8 @@ val find : forest -> int -> int
 
 val find_pac : forest -> int -> pa_constructor -> int
 
+val find_oldest_pac : forest -> int -> pa_constructor -> int
+
 val term : forest -> int -> term
 
 val get_constructor_info : forest -> int -> cinfo
@@ -105,25 +156,7 @@ val subterms : forest -> int -> int * int
 val join_path : forest -> int -> int ->
   ((int * int) * equality) list * ((int * int) * equality) list
 
-type quant_eq=
-    {qe_hyp_id: identifier;
-     qe_pol: bool;
-     qe_nvars:int;
-     qe_lhs: ccpattern;
-     qe_lhs_valid:patt_kind;
-     qe_rhs: ccpattern;
-     qe_rhs_valid:patt_kind}
-
-
-type pa_fun=
-    {fsym:int;
-     fnargs:int}
-
-type matching_problem
-
-module PafMap: Map.S with type key = pa_fun
-
-val make_fun_table : state -> Intset.t PafMap.t
+val make_fun_table : state -> Int.Set.t PafMap.t
 
 val do_match :  state ->
     (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
@@ -136,8 +169,9 @@ 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 empty_forest: unit -> forest
 
 
 
@@ -161,7 +195,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 +241,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))
 *)
 
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 037e9f66..42c03234 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,10 +9,10 @@
 (* This file uses the (non-compressed) union-find structure to generate *)
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
-open Util
-open Names
+open Errors
 open Term
 open Ccalgo
+open Pp
 
 type rule=
     Ax of constr
@@ -20,7 +20,7 @@ type rule=
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
-  | Inject of proof*constructor*int*int
+  | Inject of proof*pconstructor*int*int
 and proof =
     {p_lhs:term;p_rhs:term;p_rule:rule}
 
@@ -47,7 +47,7 @@ let rec ptrans p1 p3=
 	{p_lhs=p1.p_lhs;
 	 p_rhs=p3.p_rhs;
 	 p_rule=Trans (p1,p3)}
-      else anomaly "invalid cc transitivity"
+      else anomaly (Pp.str "invalid cc transitivity")
 
 let rec psym p =
   match p.p_rule with
@@ -85,67 +85,72 @@ let rec nth_arg t n=
 	if n>0 then
 	  nth_arg t1 (n-1)
 	else t2
-    | _ -> anomaly "nth_arg: not enough args"
+    | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args")
 
 let pinject p c n a =
   {p_lhs=nth_arg p.p_lhs (n-a);
    p_rhs=nth_arg p.p_rhs (n-a);
    p_rule=Inject(p,c,n,a)}
 
-let build_proof uf=
+let rec equal_proof uf i j=
+  debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  if i=j then prefl (term uf i) else
+    let (li,lj)=join_path uf i j in
+    ptrans (path_proof uf i li) (psym (path_proof uf j lj))
+      
+and edge_proof uf ((i,j),eq)=
+  debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  let pi=equal_proof uf i eq.lhs in
+  let pj=psym (equal_proof uf j eq.rhs) in
+  let pij=
+    match eq.rule with
+      Axiom (s,reversed)->
+	if reversed then psymax (axioms uf) s
+	else pax (axioms uf) s
+    | Congruence ->congr_proof uf eq.lhs eq.rhs
+    | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) 
+      let p=ind_proof uf ti ipac tj jpac in
+      let cinfo= get_constructor_info uf ipac.cnode in
+      pinject p cinfo.ci_constr cinfo.ci_nhyps k in  
+  ptrans (ptrans pi pij) pj
+  
+and constr_proof uf i ipac=
+  debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+  let t=find_oldest_pac uf i ipac in
+  let eq_it=equal_proof uf i t in
+  if ipac.args=[] then
+    eq_it
+  else
+    let fipac=tail_pac ipac in
+    let (fi,arg)=subterms uf t in
+    let targ=term uf arg in
+    let p=constr_proof uf fi fipac in
+    ptrans eq_it (pcongr p (prefl targ))
+      
+and path_proof uf i l=
+  debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+	   (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
+  match l with
+  | [] -> prefl (term uf i)
+  | x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
+    
+and congr_proof uf i j=
+  debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  let (i1,i2) = subterms uf i
+  and (j1,j2) = subterms uf j in
+  pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
+    
+and ind_proof uf i ipac j jpac=
+   debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+  let p=equal_proof uf i j
+  and p1=constr_proof uf i ipac
+  and p2=constr_proof uf j jpac in
+  ptrans (psym p1) (ptrans p p2)
 
-  let axioms = axioms uf in
-
-  let rec equal_proof i j=
-    if i=j then prefl (term uf i) else
-      let (li,lj)=join_path uf i j in
-	ptrans (path_proof i li) (psym (path_proof j lj))
-
-  and edge_proof ((i,j),eq)=
-    let pi=equal_proof i eq.lhs in
-    let pj=psym (equal_proof j eq.rhs) in
-    let pij=
-      match eq.rule with
-	  Axiom (s,reversed)->
-	    if reversed then psymax axioms s
-	    else pax axioms s
-	| Congruence ->congr_proof eq.lhs eq.rhs
-	| Injection (ti,ipac,tj,jpac,k) ->
-	    let p=ind_proof ti ipac tj jpac in
-	    let cinfo= get_constructor_info uf ipac.cnode in
-	      pinject p cinfo.ci_constr cinfo.ci_nhyps k
-    in  ptrans (ptrans pi pij) pj
-
-  and constr_proof i t ipac=
-    if ipac.args=[] then
-      equal_proof i t
-    else
-      let npac=tail_pac ipac in
-      let (j,arg)=subterms uf t in
-      let targ=term uf arg in
-      let rj=find uf j in
-      let u=find_pac uf rj npac in
-      let p=constr_proof j u npac in
-	ptrans (equal_proof i t) (pcongr p (prefl targ))
-
-  and path_proof i=function
-      [] -> prefl (term uf i)
-    | x::q->ptrans (path_proof (snd (fst x)) q) (edge_proof x)
-
-  and congr_proof i j=
-    let (i1,i2) = subterms uf i
-    and (j1,j2) = subterms uf j in
-      pcongr (equal_proof i1 j1) (equal_proof i2 j2)
-
-  and ind_proof i ipac j jpac=
-    let p=equal_proof i j
-    and p1=constr_proof i i ipac
-    and p2=constr_proof j j jpac in
-      ptrans (psym p1) (ptrans p p2)
-  in
-    function
-	`Prove (i,j) -> equal_proof i j
-      | `Discr (i,ci,j,cj)-> ind_proof i ci j cj
+let build_proof uf=
+  function
+  | `Prove (i,j) -> equal_proof uf i j
+  | `Discr (i,ci,j,cj)-> ind_proof uf i ci j cj
 
 
 
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index d55d3ef7..0e0eb6d2 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,14 +16,44 @@ type rule=
   | Refl of term
   | Trans of proof*proof
   | Congr of proof*proof
-  | Inject of proof*constructor*int*int
+  | Inject of proof*pconstructor*int*int
 and proof =
     private {p_lhs:term;p_rhs:term;p_rule:rule}
 
+(** Proof smart constructors *)
+
+val prefl:term -> proof
+
+val pcongr: proof -> proof -> proof
+
+val ptrans: proof -> proof -> proof
+
+val psym: proof -> proof
+
+val pax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
+           Ccalgo.Constrhash.key -> proof
+
+val psymax :  (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
+           Ccalgo.Constrhash.key -> proof
+
+val pinject :  proof -> pconstructor -> int -> int -> proof
+
+(** Proof building functions *)
+
+val equal_proof : forest -> int -> int -> proof
+
+val edge_proof : forest -> (int*int)*equality -> proof
+
+val path_proof : forest -> int -> ((int*int)*equality) list -> proof
+
+val congr_proof :  forest -> int -> int -> proof
+
+val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof
+
+(** Main proof building function *)
+
 val build_proof :
   forest ->
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
-
-
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 60d42916..7110e5b2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -1,49 +1,39 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
 (* This file is the interface between the c-c algorithm and Coq *)
 
 open Evd
-open Proof_type
 open Names
-open Libnames
-open Nameops
 open Inductiveops
 open Declarations
 open Term
+open Vars
 open Tacmach
 open Tactics
-open Tacticals
 open Typing
 open Ccalgo
-open Tacinterp
 open Ccproof
 open Pp
+open Errors
 open Util
-open Format
-
-let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
-
-let _f_equal = constant ["Init";"Logic"] "f_equal"
-
-let _eq_rect = constant ["Init";"Logic"] "eq_rect"
-
-let _refl_equal = constant ["Init";"Logic"] "eq_refl"
 
-let _sym_eq = constant ["Init";"Logic"] "eq_sym"
+let reference dir s = Coqlib.gen_reference "CC" dir s
 
-let _trans_eq = constant ["Init";"Logic"] "eq_trans"
-
-let _eq = constant ["Init";"Logic"] "eq"
-
-let _False = constant ["Init";"Logic"] "False"
+let _f_equal = reference ["Init";"Logic"] "f_equal"
+let _eq_rect = reference ["Init";"Logic"] "eq_rect"
+let _refl_equal = reference ["Init";"Logic"] "eq_refl"
+let _sym_eq = reference ["Init";"Logic"] "eq_sym"
+let _trans_eq = reference ["Init";"Logic"] "eq_trans"
+let _eq = reference ["Init";"Logic"] "eq"
+let _False = reference ["Init";"Logic"] "False"
+let _True = reference ["Init";"Logic"] "True"
+let _I = reference ["Init";"Logic"] "I"
 
 let whd env=
   let infos=Closure.create_clos_infos Closure.betaiotazeta env in
@@ -55,7 +45,8 @@ let whd_delta env=
 
 (* decompose member of equality in an applicative format *)
 
-let sf_of env sigma c = family_of_sort (sort_of env sigma c)
+(** FIXME: evar leak *)
+let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c)
 
 let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
@@ -70,32 +61,37 @@ let rec decompose_term env sigma t=
 	Appli(Appli(Product (sort_a,sort_b) ,
 		    decompose_term env sigma a),
 	      decompose_term env sigma b)
-    | Construct c->
-	let (mind,i_ind),i_con = c in 
+    | Construct c ->
+	let (((mind,i_ind),i_con),u)= c in 
 	let canon_mind = mind_of_kn (canonical_mind mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
-	let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in
-	  Constructor {ci_constr= (canon_ind,i_con);
+	let nargs=constructor_nallargs_env env (canon_ind,i_con) in
+	  Constructor {ci_constr= ((canon_ind,i_con),u);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}
     | Ind c -> 
-	let mind,i_ind = c in 
+	let (mind,i_ind),u = c in 
 	let canon_mind = mind_of_kn (canonical_mind mind) in
-	let canon_ind = canon_mind,i_ind in  (Symb (mkInd canon_ind))
-    | Const c -> 
+	let canon_ind = canon_mind,i_ind in  (Symb (mkIndU (canon_ind,u)))
+    | Const (c,u) -> 
 	let canon_const = constant_of_kn (canonical_con c) in 
-	  (Symb (mkConst canon_const))
+	  (Symb (mkConstU (canon_const,u)))
+    | Proj (p, c) -> 
+	let canon_const kn = constant_of_kn (canonical_con kn) in 
+	let p' = Projection.map canon_const p in
+	  (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
     | _ ->if closed0 t then (Symb t) else raise Not_found
 
 (* decompose equality in members and type *)
+open Globnames
 
 let atom_of_constr env sigma term =
   let wh =  (whd_delta env term) in
   let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3
+	if is_global _eq f && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -107,9 +103,9 @@ let rec pattern_of_constr env sigma c =
       App (f,args)->
 	let pf = decompose_term env sigma f in
 	let pargs,lrels = List.split
-	  (array_map_to_list (pattern_of_constr env sigma) args) in
+	  (Array.map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
-	List.fold_left Intset.union Intset.empty lrels
+	List.fold_left Int.Set.union Int.Set.empty lrels
     | 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
@@ -117,11 +113,11 @@ let rec pattern_of_constr env sigma c =
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	  PApp(Product (sort_a,sort_b),
-	       [pa;pb]),(Intset.union sa sb)
-    | Rel i -> PVar i,Intset.singleton i
+	       [pa;pb]),(Int.Set.union sa sb)
+    | Rel i -> PVar i,Int.Set.singleton i
     | _ ->
 	let pf = decompose_term env sigma c in
-	  PApp (pf,[]),Intset.empty
+	  PApp (pf,[]),Int.Set.empty
 
 let non_trivial = function
     PVar _ -> false
@@ -129,23 +125,21 @@ let non_trivial = function
 
 let patterns_of_constr env sigma nrels term=
   let f,args=
-    try destApp (whd_delta env term)
-    with e when Errors.noncritical e -> raise Not_found
-  in
-	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
+    try destApp (whd_delta env term) with DestKO -> raise Not_found in
+	if is_global _eq f && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
 	  let valid1 =
-	    if Intset.cardinal rels1 <> nrels then Creates_variables
+	    if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
 	    else if non_trivial patt1 then Normal
 	    else Trivial args.(0)
 	  and valid2 =
-	    if Intset.cardinal rels2 <> nrels then Creates_variables
+	    if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
 	    else if non_trivial patt2 then Normal
 	    else Trivial args.(0) in
-	    if valid1 <> Creates_variables
-	      || valid2 <> Creates_variables  then
+	    if valid1 != Creates_variables
+	      || valid2 != Creates_variables  then
 	      nrels,valid1,patt1,valid2,patt2
 	    else raise Not_found
 	else raise Not_found
@@ -153,7 +147,7 @@ let patterns_of_constr env sigma nrels term=
 let rec quantified_atom_of_constr env sigma nrels term =
   match kind_of_term (whd_delta env term) with
       Prod (id,atom,ff) -> 
-	if eq_constr ff (Lazy.force _False) then
+	if is_global _False ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
@@ -165,7 +159,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 let litteral_of_constr env sigma term=
   match kind_of_term (whd_delta env term) with
     | Prod (id,atom,ff) -> 
-	if eq_constr ff (Lazy.force _False) then
+	if is_global _False ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
 	    | `Other(p) -> `Nother(p)
@@ -182,7 +176,7 @@ let litteral_of_constr env sigma term=
 
 (* store all equalities from the context *)
 
-let rec make_prb gls depth additionnal_terms =
+let make_prb gls depth additionnal_terms =
   let env=pf_env gls in
   let sigma=sig_sig gls in
   let state = empty depth gls in
@@ -213,9 +207,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 (Goal.V82.hyps gls.sigma gls.it));
+	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
     begin
-      match atom_of_constr env sigma (pf_concl gls) with
+      match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->
 		  List.iter
@@ -226,226 +220,256 @@ let rec make_prb gls depth additionnal_terms =
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
 
-let build_projection intype outtype (cstr:constructor) special default gls=
+let build_projection intype outtype (cstr:pconstructor) special default gls=
   let env=pf_env gls in
-  let (h,argv) =
-    try destApp intype with
-	Invalid_argument _ -> (intype,[||])  in
-  let ind=destInd h in
-  let types=Inductiveops.arities_of_constructors env ind in
+  let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in
+  let ind,u=destInd h in
+  let types=Inductiveops.arities_of_constructors env (ind,u) in
   let lp=Array.length types in
-  let ci=pred (snd cstr) in
+  let ci=pred (snd(fst cstr)) in
   let branch i=
-    let ti=Term.prod_appvect types.(i) argv in
+    let ti= prod_appvect types.(i) argv in
     let rc=fst (decompose_prod_assum ti) in
     let head=
-      if i=ci then special else default in
+      if Int.equal i ci then special else default in
       it_mkLambda_or_LetIn head rc in
   let branches=Array.init lp branch in
   let casee=mkRel 1 in
   let pred=mkLambda(Anonymous,intype,outtype) in
   let case_info=make_case_info (pf_env gls) ind RegularStyle in
   let body= mkCase(case_info, pred, casee, branches) in
-  let id=pf_get_new_id (id_of_string "t") gls in
+  let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
 
 let _M =mkMeta
 
-let rec proof_tac p gls =
+let app_global f args k = 
+  Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+
+let new_app_global f args k = 
+  Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args)))
+
+let new_refine c = Proofview.V82.tactic (refine c)
+
+let rec proof_tac p : unit Proofview.tactic =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let type_of t = Tacmach.New.pf_type_of gl t in
+  try (* type_of can raise exceptions *)
   match p.p_rule with
-      Ax c -> exact_check c gls
+      Ax c -> exact_check c
     | SymAx c ->
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
-        let typ = Termops.refresh_universes (pf_type_of gls l) in
-	  exact_check
-	    (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls
+        let typ = (* Termops.refresh_universes *) type_of l in
+        new_app_global _sym_eq [|typ;r;l;c|] exact_check
     | Refl t ->
 	let lr = constr_of_term t 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
+	let typ = (* Termops.refresh_universes *) type_of lr in
+        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check
     | 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 = 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
+	let typ = (* Termops.refresh_universes *) (type_of t2) in
+	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
+          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	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 = 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 typf = (* Termops.refresh_universes  *)(type_of tf1) in
+	let typx = (* Termops.refresh_universes *) (type_of tx1) in
+	let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in
+        let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
-	  mkApp(Lazy.force _f_equal,
-		[|typf;typfx;appx1;tf1;tf2;_M 1|]) in
+	  app_global _f_equal
+		[|typf;typfx;appx1;tf1;tf2;_M 1|] in
 	let lemma2=
-	  mkApp(Lazy.force _f_equal,
-		[|typx;typfx;tf2;tx1;tx2;_M 1|]) in
+	  app_global _f_equal
+		[|typx;typfx;tf2;tx1;tx2;_M 1|] in
 	let prf =
-	  mkApp(Lazy.force _trans_eq,
+	  app_global _trans_eq
 		[|typfx;
 		  mkApp(tf1,[|tx1|]);
 		  mkApp(tf2,[|tx1|]);
-		  mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in
-	  tclTHENS (refine prf)
-	    [tclTHEN (refine lemma1) (proof_tac p1);
-  	     tclFIRST
-	       [tclTHEN (refine lemma2) (proof_tac p2);
+		  mkApp(tf2,[|tx2|]);_M 2;_M 3|] in
+	  Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine))
+	    [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1);
+  	     Tacticals.New.tclFIRST
+	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
 		reflexivity;
-		fun gls ->
-		  errorlabstrm  "Congruence"
+                Proofview.tclZERO (UserError ("Congruence" ,
 		    (Pp.str
-		       "I don't know how to handle dependent equality")]] gls
+		       "I don't know how to handle dependent equality")))]]
   | Inject (prf,cstr,nargs,argind) ->
 	 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 = Termops.refresh_universes (pf_type_of gls ti) in
-	 let outtype = Termops.refresh_universes (pf_type_of gls default) in
+	 let intype = (* Termops.refresh_universes *) (type_of ti) in
+	 let outtype = (* Termops.refresh_universes *) (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
-	 let proj=build_projection intype outtype cstr special default gls in
+         let proj =
+           Tacmach.New.of_old (build_projection intype outtype cstr special default) gl
+         in
 	 let injt=
-	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
-	   tclTHEN (refine injt) (proof_tac prf) gls
+           app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
+  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
-let refute_tac c t1 t2 p gls =
+let refute_tac c t1 t2 p =
+  Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype = Termops.refresh_universes (pf_type_of gls tt1) in
-  let neweq=
-    mkApp(Lazy.force _eq,
-	  [|intype;tt1;tt2|]) in
-  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let intype =
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl
+  in
+  let neweq= new_app_global _eq [|intype;tt1;tt2|] in
+  let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
-    tclTHENS (assert_tac (Name hid) neweq)
-      [proof_tac p; simplest_elim false_t] gls
+    Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+      [proof_tac p; simplest_elim false_t]
+  end
 
-let convert_to_goal_tac c t1 t2 p gls =
+let refine_exact_check c gl =
+  let evm, _ = pf_apply e_type_of gl c in
+    Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
+
+let convert_to_goal_tac c t1 t2 p = 
+  Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 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
+  let sort =
+    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl
+  in
+  let neweq= new_app_global _eq [|sort;tt1;tt2|] in
+  let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
+  let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
   let identity=mkLambda (Name x,sort,mkRel 1) in
-  let endt=mkApp (Lazy.force _eq_rect,
-		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
-    tclTHENS (assert_tac (Name e) neweq)
-      [proof_tac p;exact_check endt] gls
+  let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+    Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
+      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+  end
 
-let convert_to_hyp_tac c1 t1 c2 t2 p gls =
+let convert_to_hyp_tac c1 t1 c2 t2 p =
+  Proofview.Goal.nf_enter begin fun gl ->
   let tt2=constr_of_term t2 in
-  let h=pf_get_new_id (id_of_string "H") gls in
+  let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
-    tclTHENS (assert_tac (Name h) tt2)
+    Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
-       simplest_elim false_t] 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 = Termops.refresh_universes (pf_type_of gls t1) in
-  let concl=pf_concl gls 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 (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
-  let injt=mkApp (Lazy.force _f_equal,
-		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in
-  let endt=mkApp (Lazy.force _eq_rect,
-		  [|outtype;trivial;pred;identity;concl;injt|]) in
-  let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
-    tclTHENS (assert_tac (Name hid) neweq)
-      [proof_tac p;exact_check endt] gls
+       simplest_elim false_t]
+  end
+
+let discriminate_tac (cstr,u as cstru) p =
+  Proofview.Goal.nf_enter begin fun gl ->
+    let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+    let intype =
+      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl
+    in
+    let concl = Proofview.Goal.concl gl in
+    (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
+    (* let outsort = mkSort outsort in *)
+    let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
+    (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
+    let identity = Universes.constr_of_global _I in
+    (* let trivial=pf_type_of gls identity in *)
+    let trivial = Universes.constr_of_global _True in
+    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
+    let outtype = mkSort outtype in
+    let pred=mkLambda(Name xid,outtype,mkRel 1) in
+    let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
+    let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in
+    let injt=app_global _f_equal
+                    [|intype;outtype;proj;t1;t2;mkVar hid|] in
+    let endt k =
+      injt (fun injt ->
+        app_global _eq_rect
+          [|outtype;trivial;pred;identity;concl;injt|] k) in
+    let neweq=new_app_global _eq [|intype;t1;t2|] in
+    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
+      (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+        [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
+  end
 
 (* wrap everything *)
 
 let build_term_to_complete uf meta pac =
   let cinfo = get_constructor_info uf pac.cnode in
   let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in
-  let dummy_args = List.rev (list_tabulate meta pac.arity) in
+  let dummy_args = List.rev (List.init pac.arity meta) in
   let all_args = List.rev_append real_args dummy_args in
-    applistc (mkConstruct cinfo.ci_constr) all_args
-
-let cc_tactic depth additionnal_terms gls=
-  Coqlib.check_required_library ["Coq";"Init";"Logic"];
-  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
-  let state = make_prb gls depth additionnal_terms in
-  let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in
-  let sol = execute true state in
-  let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
-  let uf=forest state in
+    applistc (mkConstructU cinfo.ci_constr) all_args
+
+let cc_tactic depth additionnal_terms =
+  Proofview.Goal.nf_enter begin fun gl ->
+    Coqlib.check_required_library Coqlib.logic_module_name;
+    let _ = debug (Pp.str "Reading subgoal ...") in
+    let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
+    let _ = debug (Pp.str "Problem built, solving ...") in
+    let sol = execute true state in
+    let _ = debug (Pp.str "Computation completed.") in
+    let uf=forest state in
     match sol with
-	None -> tclFAIL 0 (str "congruence failed") gls
-      | Some reason ->
-	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
-	  match reason with
-	      Discrimination (i,ipac,j,jpac) ->
-		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
-		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
-		  discriminate_tac cstr p gls
-	    | Incomplete ->
-		let metacnt = ref 0 in
-		let newmeta _ = incr metacnt; _M !metacnt in
-		let terms_to_complete =
-		  List.map
-		    (build_term_to_complete uf newmeta)
-		    (epsilons uf) in
-		  Pp.msgnl
-		    (Pp.str "Goal is solvable by congruence but \
+      None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
+    | Some reason ->
+	debug (Pp.str "Goal solved, generating proof ...");
+	match reason with
+	  Discrimination (i,ipac,j,jpac) ->
+	    let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
+	    let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+	    discriminate_tac cstr p
+	| Incomplete ->
+            let env = Proofview.Goal.env gl in
+	    let metacnt = ref 0 in
+	    let newmeta _ = incr metacnt; _M !metacnt in
+	    let terms_to_complete =
+	      List.map
+		(build_term_to_complete uf newmeta)
+		(epsilons uf) in
+	    Pp.msg_info
+	      (Pp.str "Goal is solvable by congruence but \
  some arguments are missing.");
-		  Pp.msgnl
-		    (Pp.str "  Try " ++
-		     hov 8
-		       begin
-			 str "\"congruence with (" ++
-			 prlist_with_sep
-			   (fun () -> str ")" ++ pr_spc () ++ str "(")
-			   (Termops.print_constr_env (pf_env gls))
-			   terms_to_complete ++
-			 str ")\","
-		       end);
-		  Pp.msgnl
-		    (Pp.str "  replacing metavariables by arbitrary terms.");
-		  tclFAIL 0 (str "Incomplete") gls
-	    | Contradiction dis ->
-		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
-		let ta=term uf dis.lhs and tb=term uf dis.rhs in
-		  match dis.rule with
-		      Goal -> proof_tac p gls
-		    | Hyp id -> refute_tac id ta tb p gls
-		    | HeqG id ->
-			convert_to_goal_tac id ta tb p gls
-		    | HeqnH (ida,idb) ->
-			convert_to_hyp_tac ida ta idb tb p gls
-
+	    Pp.msg_info
+	      (Pp.str "  Try " ++
+		 hov 8
+		 begin
+		   str "\"congruence with (" ++
+		     prlist_with_sep
+		     (fun () -> str ")" ++ spc () ++ str "(")
+		     (Termops.print_constr_env env)
+		     terms_to_complete ++
+		     str ")\","
+		 end ++
+		 Pp.str "  replacing metavariables by arbitrary terms.");
+	    Tacticals.New.tclFAIL 0 (str "Incomplete")
+	| Contradiction dis ->
+	    let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+	    let ta=term uf dis.lhs and tb=term uf dis.rhs in
+	    match dis.rule with
+	      Goal -> proof_tac p
+	    | Hyp id -> refute_tac id ta tb p
+	    | HeqG id ->
+		convert_to_goal_tac id ta tb p
+	    | HeqnH (ida,idb) ->
+		convert_to_hyp_tac ida ta idb tb p
+  end
 
 let cc_fail gls =
   errorlabstrm  "Congruence" (Pp.str "congruence failed.")
 
 let congruence_tac depth l =
-  tclORELSE
-    (tclTHEN (tclREPEAT introf) (cc_tactic depth l))
-    cc_fail
+  Tacticals.New.tclORELSE
+    (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
+    (Proofview.V82.tactic cc_fail)
 
 (* Beware: reflexivity = constructor 1 = apply refl_equal
    might be slow now, let's rather do something equivalent
    to a "simple apply refl_equal" *)
 
-let simple_reflexivity () = apply (Lazy.force _refl_equal)
-
 (* The [f_equal] tactic.
 
    It mimics the use of lemmas [f_equal], [f_equal2], etc.
@@ -453,22 +477,35 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
    the fact that congruence is called internally.
 *)
 
-let f_equal gl =
-  let cut_eq c1 c2 =
-    let ty = Termops.refresh_universes (pf_type_of gl c1) in
-    tclTHENTRY
-      (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
-      (simple_reflexivity ())
-  in
-  try match kind_of_term (pf_concl gl) with
-    | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
-	begin match kind_of_term t, kind_of_term t' with
-	  | App (f,v), App (f',v') when Array.length v = Array.length v' ->
+let f_equal =
+  Proofview.Goal.nf_enter begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
+    let type_of = Tacmach.New.pf_type_of gl in
+    let cut_eq c1 c2 =
+      try (* type_of can raise an exception *)
+        let ty = (* Termops.refresh_universes *) (type_of c1) in
+        if eq_constr_nounivs c1 c2 then Proofview.tclUNIT ()
+        else
+          Tacticals.New.tclTRY (Tacticals.New.tclTHEN
+          ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut)
+          (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)))
+      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    in
+    Proofview.tclORELSE
+      begin match kind_of_term concl with
+      | App (r,[|_;t;t'|]) when Globnames.is_global _eq r ->
+	  begin match kind_of_term t, kind_of_term t' with
+	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
-		if i < 0 then tclTRY (congruence_tac 1000 [])
-		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
-	      in cuts (Array.length v - 1) gl
-	  | _ -> tclIDTAC gl
-	end
-    | _ -> tclIDTAC gl
-  with Type_errors.TypeError _ -> tclIDTAC gl
+		if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
+		else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+	      in cuts (Array.length v - 1)
+	  | _ -> Proofview.tclUNIT ()
+	  end
+      | _ -> Proofview.tclUNIT ()
+      end
+      begin function (e, info) -> match e with
+        | Type_errors.TypeError _ -> Proofview.tclUNIT ()
+        | e -> Proofview.tclZERO ~info e
+      end
+  end
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 60a1b2ec..7c1d9f1c 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -1,6 +1,7 @@
+
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,12 +10,12 @@
 open Term
 open Proof_type
 
-val proof_tac: Ccproof.proof -> Proof_type.tactic
+val proof_tac: Ccproof.proof -> unit Proofview.tactic
 
-val cc_tactic : int -> constr list -> tactic
+val cc_tactic : int -> constr list ->  unit Proofview.tactic
 
 val cc_fail : tactic
 
-val congruence_tac : int -> constr list -> tactic
+val congruence_tac : int -> constr list -> unit Proofview.tactic
 
-val f_equal : tactic
+val f_equal : unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 8b3fe770..aa31c6f0 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -1,16 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Cctac
-open Tactics
-open Tacticals
+
+DECLARE PLUGIN "cc_plugin"
 
 (* Tactic registration *)