First debug... the renaming of librairies was not working and auto/dn were not taking in account equivalent names of inductive types.

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

1 files changed, 4 insertions, 5 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index ec4a1260c..9acdd1585 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -102,8 +102,8 @@ let rec pattern_of_constr t =
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
     | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
     | Const sp         -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
-    | Ind sp        -> PRef (IndRef sp)
-    | Construct sp -> PRef (ConstructRef sp)
+    | Ind sp        -> PRef (canonical_gr (IndRef sp))
+    | Construct sp -> PRef (canonical_gr (ConstructRef sp))
     | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
     | Case (ci,p,a,br) ->
 	let cip = ci.ci_pp_info in
@@ -212,9 +212,8 @@ let rec pat_of_raw metas vars = function
        with Not_found -> PVar id)
   | RPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
-  | RRef (_,ConstRef con) ->
-      PRef (ConstRef (constant_of_kn(canonical_con con)))
-  | RRef (_,r) -> PRef r
+  | RRef (_,gr) ->
+      PRef (canonical_gr gr)
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
   | RApp (_, RPatVar (_,(true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)