1 files changed, 33 insertions, 5 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a21137a05..25817478e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -19,6 +19,16 @@ open Ltac_pretype
 
 let cases_pattern_loc c = c.CAst.loc
 
+let alias_of_pat pat = DAst.with_val (function
+  | PatVar name -> name
+  | PatCstr(_,_,name) -> name
+  ) pat
+
+let set_pat_alias id = DAst.map (function
+  | PatVar Anonymous -> PatVar (Name id)
+  | PatCstr (cstr,patl,Anonymous) -> PatCstr (cstr,patl,Name id)
+  | pat -> assert false)
+
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
@@ -452,6 +462,10 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
 (**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
 
+let is_gvar id c = match DAst.get c with
+| GVar id' -> Id.equal id id'
+| _ -> false
+
 let rec cases_pattern_of_glob_constr na = DAst.map (function
   | GVar id ->
     begin match na with
@@ -468,6 +482,9 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
       PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
     | _ -> raise Not_found
     end
+  | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous ->
+     (* A canonical encoding of aliases *)
+     DAst.get (cases_pattern_of_glob_constr na' b)
   | _ -> raise Not_found
   )
 
@@ -503,23 +520,34 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
       drop_local_defs typi l in
   Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
 
+let add_alias ?loc na c =
+  match na with
+  | Anonymous -> c
+  | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
+
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = DAst.map_with_loc (fun ?loc -> function
-  | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
-  | PatCstr (cstr,l,Anonymous)  ->
+let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function
+  | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None))
+  | PatCstr (cstr,l,na)  ->
       let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
       let l = add_patterns_for_params_remove_local_defs cstr l in
-      GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
+      add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l))
+  | PatVar (Name id) when not isclosed ->
+      GVar id
+  | PatVar Anonymous when not isclosed ->
+      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
   | _ -> raise Not_found
   ) x
 
 let glob_constr_of_closed_cases_pattern p = match DAst.get p with
   | PatCstr (cstr,l,na) ->
       let loc = p.CAst.loc in
-      na,glob_constr_of_closed_cases_pattern_aux (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
+      na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
 
+let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
+
 (**********************************************************************)
 (* Interpreting ltac variables *)