diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 6 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 4 | ||||
| -rw-r--r-- | pretyping/patternops.mli | 1 |
3 files changed, 6 insertions, 5 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 1264b0b33c..02c2fc4a13 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -34,10 +34,10 @@ let cases_predicate_names tml = | (tm,(na,None)) -> [na] | (tm,(na,Some {v=(_,nal)})) -> na::nal) tml) -let mkGApp ?loc p t = DAst.make ?loc @@ +let mkGApp ?loc p l = DAst.make ?loc @@ match DAst.get p with - | GApp (f,l) -> GApp (f,l@[t]) - | _ -> GApp (p,[t]) + | GApp (f,l') -> GApp (f,l'@l) + | _ -> GApp (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 index 37aa31d094..20ac35888e 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -42,8 +42,8 @@ val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list -(** Apply one argument to a glob_constr *) -val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_constr_g +(** 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 map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 304e06818e..342891d65f 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -37,6 +37,7 @@ val head_pattern_bound : constr_pattern -> GlobRef.t returns its label; raises an anomaly otherwise *) val head_of_constr_reference : Evd.evar_map -> constr -> GlobRef.t +[@@ocaml.deprecated "use [EConstr.destRef]"] (** [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no |