Adding ability to put any pattern in binders, prefixed by a quote.

Cf CHANGES for details.

1 files changed, 14 insertions, 3 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 82fa85f69..99b229251 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -765,6 +765,7 @@ let rec extern inctx scopes vars r =
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
+                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -781,7 +782,8 @@ let rec extern inctx scopes vars r =
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
-                 let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in
+                 let (_,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
 		 ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
@@ -824,13 +826,13 @@ and factorize_lambda inctx scopes vars na bk aty c =
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
-  | (na,bk,Some bd,ty)::l ->
+  | (Inl na,bk,Some bd,ty)::l ->
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
        LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l)
 
-  | (na,bk,None,ty)::l ->
+  | (Inl na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
           (assums,ids,LocalRawAssum(nal,k,ty')::l)
@@ -843,6 +845,14 @@ and extern_local_binder scopes vars = function
             (na::assums,na::ids,
              LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l))
 
+  | (Inr p,bk,Some bd,ty)::l -> assert false
+
+  | (Inr p,bk,None,ty)::l ->
+      let ty = extern_typ scopes vars ty in
+      let p = extern_cases_pattern vars p in
+      let (assums,ids,l) = extern_local_binder scopes vars l in
+      (assums,ids, LocalPattern(Loc.ghost,p,Some ty) :: l)
+
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
@@ -1050,4 +1060,5 @@ let extern_constr_pattern env sigma pat =
 let extern_rel_context where env sigma sign =
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
+  let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in
   pi3 (extern_local_binder (None,[]) vars a)