- Structuring Numbers and fixing Setoid in stdlib's doc.

- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True").



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

3 files changed, 41 insertions, 20 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c658faa0f..87768c419 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -191,11 +191,14 @@ let set_var_scope loc id (_,_,scopt,scopes) varscopes =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
-let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env))=
+ function
+ | Anonymous -> (renaming,env),Anonymous
+ | Name id ->
   try
     (* Binders bound in the notation are considered first-order objects *)
-    let _,id' = coerce_to_id (fst (List.assoc id subst)) in
-    (renaming,(Idset.add id' ids,unb,tmpsc,scopes)), id'
+    let _,na = coerce_to_name (fst (List.assoc id subst)) in
+    (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -205,7 +208,7 @@ let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) i
     let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
     let id' = next_ident_away id fvs in
     let renaming' = if id=id' then renaming else (id,id')::renaming in
-    (renaming',env), id'
+    (renaming',env), Name id'
 
 let rec subst_iterator y t = function
   | RVar (_,id) as x -> if id = y then t else x
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 6bee22f6c..d31230552 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -53,11 +53,17 @@ type aconstr =
 (**********************************************************************)
 (* Re-interpret a notation as a rawconstr, taking care of binders     *)
 
+let name_to_ident = function
+  | Anonymous -> error "This expression should be a simple identifier."
+  | Name id -> id 
+
+let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
+
 let rec cases_pattern_fold_map loc g e = function
   | PatVar (_,na) ->
-      let e',na' = name_fold_map g e na in e', PatVar (loc,na')
+      let e',na' = g e na in e', PatVar (loc,na')
   | PatCstr (_,cstr,patl,na) ->
-      let e',na' = name_fold_map g e na in
+      let e',na' = g e na in
       let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in
       e', PatCstr (loc,cstr,patl',na')
 
@@ -77,38 +83,38 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
       subst_rawvars outerl it
   | ALambda (na,ty,c) ->
-      let e,na = name_fold_map g e na in RLambda (loc,na,Explicit,f e ty,f e c)
+      let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
   | AProd (na,ty,c) ->
-      let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
+      let e,na = g e na in RProd (loc,na,Explicit,f e ty,f e c)
   | ALetIn (na,b,c) ->
-      let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
+      let e,na = g e na in RLetIn (loc,na,f e b,f e c)
   | ACases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
 	| Some (ind,npar,nal) -> 
 	  let e',nal' = List.fold_right (fun na (e',nal) -> 
-	      let e',na' = name_fold_map g e' na in e',na'::nal) nal (e',[]) in
+	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
 	  e',Some (loc,ind,npar,nal') in
-	let e',na' = name_fold_map g e' na in
+	let e',na' = g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) id = let (e,id) = g e id in ((id::idl,e),id) in
+      let fold (nal,e) na = let (e,na) = g e na in ((name_to_ident na::nal,e),na) in
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
 	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
 	(loc,idl,patl,f e rhs)) eqnl in
       RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
-      let e,nal = list_fold_map (name_fold_map g) e nal in 
-      let e,na = name_fold_map g e na in
+      let e,nal = list_fold_map g e nal in 
+      let e,na = g e na in
       RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
-      let e,na = name_fold_map g e na in
+      let e,na = g e na in
       RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
   | ARec (fk,idl,dll,tl,bl) ->
-      let e,idl = array_fold_map g e idl in
+      let e,idl = array_fold_map (to_id g) e idl in
       let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
-	  let e,na = name_fold_map g e na in
+	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
   | ACast (c,k) -> RCast (loc,f e c, 
@@ -452,9 +458,13 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | Some t1, Some t2 -> f sigma t1 t2
   | _ -> raise No_match
 
+let rawconstr_of_name = function
+  | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
+  | Name id -> RVar (dummy_loc,id)
+
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (Name id1,Name id2) when List.mem id2 metas ->
-      alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
+  | (na,Name id2) when List.mem id2 metas ->
+      alp, bind_env alp sigma id2 (rawconstr_of_name na)
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
@@ -886,6 +896,13 @@ let coerce_to_id = function
         (constr_loc a,"coerce_to_id",
          str "This expression should be a simple identifier.")
 
+let coerce_to_name = function
+  | CRef (Ident (loc,id)) -> (loc,Name id)
+  | CHole (loc,_) -> (loc,Anonymous)
+  | a -> user_err_loc
+        (constr_loc a,"coerce_to_name",
+         str "This expression should be a name.")
+
 (* Used in correctness and interface *)
 
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index cecea239c..303926967 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -62,7 +62,7 @@ val eq_rawconstr : rawconstr -> rawconstr -> bool
 (* Re-interpret a notation as a rawconstr, taking care of binders     *)
 
 val rawconstr_of_aconstr_with_binders : loc -> 
-  ('a -> identifier -> 'a * identifier) ->
+  ('a -> name -> 'a * name) ->
   ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
 
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
@@ -201,6 +201,7 @@ val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
 val coerce_to_id : constr_expr -> identifier located
+val coerce_to_name : constr_expr -> name located
 
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr