Move Record desugaring to constrintern and add ability to use notations

for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).


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

2 files changed, 9 insertions, 4 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index 04ab34baaf..bf02efb03f 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -24,6 +24,11 @@ type global_reference =
 
 let isVarRef = function VarRef _ -> true | _ -> false
 
+let subst_constructor subst ((kn,i),j as ref) =
+  let kn' = subst_kn subst kn in 
+    if kn==kn' then ref, mkConstruct ref
+    else ((kn',i),j), mkConstruct ((kn',i),j)
+      
 let subst_global subst ref = match ref with
   | VarRef var -> ref, mkVar var
   | ConstRef kn ->
@@ -32,10 +37,9 @@ let subst_global subst ref = match ref with
   | IndRef (kn,i) ->
       let kn' = subst_kn subst kn in
       if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
-  | ConstructRef ((kn,i),j) ->
-      let kn' = subst_kn subst kn in 
-      if kn==kn' then ref, mkConstruct ((kn,i),j)
-      else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j)
+  | ConstructRef ((kn,i),j as c) ->
+      let c',t = subst_constructor subst c in
+	if c'==c then ref,t else ConstructRef c', t
 
 let global_of_constr c = match kind_of_term c with
   | Const sp -> ConstRef sp
diff --git a/library/libnames.mli b/library/libnames.mli
index 890a442e39..399387dd76 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -25,6 +25,7 @@ type global_reference =
 
 val isVarRef : global_reference -> bool
 
+val subst_constructor : substitution -> constructor -> constructor * constr
 val subst_global : substitution -> global_reference -> global_reference * constr
 
 (* Turn a global reference into a construction *)