Mini-simplification

coq · Jul 4, 2021 · 9a4de81 · 9a4de81
1 parent c72ef4a
commit 9a4de81
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 12 deletions.
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
@@ -329,7 +329,7 @@ let apply_cases_pattern ?loc (ids_disjpat,id) c =
 let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_status_fun) e nc =
   let lt x = DAst.make ?loc x in lt @@ match nc with
   | NVar id -> GVar id
-  | NApp (a,args) -> let e = h.no e in DAst.get (mkGApp (f e a) (List.map (f e) args))
+  | NApp (a,args) -> let e = h.no e in mkGAppR (f e a) (List.map (f e) args)
   | NProj (p,args,c) -> let e = h.no e in GProj (p, List.map (f e) args, f e c)
   | NList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
@@ -796,13 +796,7 @@ and detype_r d flags avoid env sigma t =
     | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma (LocalAssum (na,ty)) c
     | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma (LocalDef (na,b,ty)) c
     | App (f,args) ->
-      let mkapp f' args' =
-        match DAst.get f' with
-        | GApp (f',args'') ->
-          GApp (f',args''@args')
-        | _ -> GApp (f',args')
-      in
-      mkapp (detype d flags avoid env sigma f)
+      Glob_ops.mkGAppR (detype d flags avoid env sigma f)
         (Array.map_to_list (detype d flags avoid env sigma) args)
     | Const (sp,u) -> GRef (GlobRef.ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
@@ -34,10 +34,13 @@ let cases_predicate_names tml =
     | (tm,(na,None)) -> [na]
     | (tm,(na,Some {v=(_,nal)})) -> na::nal) tml)
 
-let mkGApp ?loc p l = DAst.make ?loc @@
-  match DAst.get p with
-  | GApp (f,l') -> GApp (f,l'@l)
-  | _          -> GApp (p,l)
+let mkGAppR f args =
+  match DAst.get f with
+  | GApp (f',args') -> GApp (f',args'@args)
+  | _ -> GApp (f,args)
+
+let mkGApp ?loc p l =
+  DAst.make ?loc @@ mkGAppR p l
 
 let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp1 = Option.map f obd in

diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
@@ -50,6 +50,7 @@ val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list
 
 (** Apply a list of arguments to a glob_constr *)
 val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g list -> 'a glob_constr_g
+val mkGAppR : 'a glob_constr_g -> 'a glob_constr_g list -> 'a glob_constr_r
 
 val map_glob_constr :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr