commit 13400 and 13409.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13410 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 36 insertions, 3 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 5ab435a92f..18dbecb667 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -337,6 +337,28 @@ and make_app l=function
     Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
   | other -> applistc (constr_of_term other) l
 
+let rec canonize_name c =
+  let func =  canonize_name in
+    match kind_of_term c with
+      | Const kn ->
+	  let canon_const = constant_of_kn (canonical_con kn) in 
+	    (mkConst canon_const)
+      | Ind (kn,i) ->
+	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	    (mkInd (canon_mind,i))
+      | Construct ((kn,i),j) ->
+	  let canon_mind = mind_of_kn (canonical_mind kn) in
+	    mkConstruct ((canon_mind,i),j) 
+      | Prod (na,t,ct) ->
+	  mkProd (na,func t, func ct)
+      | Lambda (na,t,ct) ->
+	  mkLambda (na, func t,func ct)
+      | LetIn (na,b,t,ct) ->
+	  mkLetIn (na, func b,func t,func ct)
+      | App (ct,l) ->
+	  mkApp (func ct,array_smartmap func l)
+      | _ -> c
+
 (* rebuild a term from a pattern and a substitution *)
 
 let build_subst uf subst =
@@ -364,6 +386,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
 	  let typ = pf_type_of state.gls (constr_of_term t) in
+	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index eb34097b17..1054b6ecd1 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -72,11 +72,21 @@ let rec decompose_term env sigma t=
 		    decompose_term env sigma a),
 	      decompose_term env sigma b)
     | Construct c->
-	let (oib,_)=Global.lookup_inductive (fst c) in
-	let nargs=mis_constructor_nargs_env env c in
-	  Constructor {ci_constr=c;
+	let (mind,i_ind),i_con = 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);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}
+    | Ind c -> 
+	let mind,i_ind = 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_const = constant_of_kn (canonical_con c) in 
+	  (Symb (mkConst canon_const))
     | _ ->if closed0 t then (Symb t) else raise Not_found
 
 (* decompose equality in members and type *)