aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml3
-rw-r--r--pretyping/cases.mli7
-rw-r--r--pretyping/constr_matching.ml1
-rw-r--r--pretyping/constr_matching.mli1
-rw-r--r--pretyping/detyping.ml1
-rw-r--r--pretyping/detyping.mli1
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/evarsolve.ml12
-rw-r--r--pretyping/glob_ops.ml1
-rw-r--r--pretyping/glob_ops.mli4
-rw-r--r--pretyping/ltac_pretype.ml68
-rw-r--r--pretyping/nativenorm.ml50
-rw-r--r--pretyping/patternops.ml25
-rw-r--r--pretyping/patternops.mli3
-rw-r--r--pretyping/pretyping.ml1
-rw-r--r--pretyping/pretyping.mli1
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/recordops.ml33
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/retyping.ml1
-rw-r--r--pretyping/tacred.mli1
-rw-r--r--pretyping/unification.ml8
22 files changed, 165 insertions, 66 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 08ce72932a..aefa09dbe6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -33,6 +33,7 @@ open Evarsolve
open Evarconv
open Evd
open Context.Rel.Declaration
+open Ltac_pretype
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
@@ -245,7 +246,7 @@ let push_history_pattern n pci cont =
type 'a pattern_matching_problem =
{ env : env;
- lvar : Glob_term.ltac_var_map;
+ lvar : Ltac_pretype.ltac_var_map;
evdref : evar_map ref;
pred : constr;
tomatch : tomatch_stack;
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 7bdc604b88..cbf5788e48 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -14,6 +14,7 @@ open EConstr
open Inductiveops
open Glob_term
open Evarutil
+open Ltac_pretype
(** {5 Compilation of pattern-matching } *)
@@ -101,7 +102,7 @@ and pattern_continuation =
type 'a pattern_matching_problem =
{ env : env;
- lvar : Glob_term.ltac_var_map;
+ lvar : Ltac_pretype.ltac_var_map;
evdref : evar_map ref;
pred : constr;
tomatch : tomatch_stack;
@@ -119,11 +120,11 @@ val prepare_predicate : ?loc:Loc.t ->
Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
Environ.env ->
Evd.evar_map ->
- Glob_term.ltac_var_map ->
+ Ltac_pretype.ltac_var_map ->
(types * tomatch_type) list ->
(rel_context * rel_context) list ->
constr option ->
glob_constr option -> (Evd.evar_map * Names.name list * constr) list
val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name ->
- Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map
+ Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0973d73ee0..9128d4042b 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -22,6 +22,7 @@ open Pattern
open Patternops
open Misctypes
open Context.Rel.Declaration
+open Ltac_pretype
(*i*)
(* Given a term with second-order variables in it,
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 1d7019d09f..34c62043ef 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -13,6 +13,7 @@ open Term
open EConstr
open Environ
open Pattern
+open Ltac_pretype
type binding_bound_vars = Id.Set.t
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f3e8e72bb7..c02fc5aafd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -27,6 +27,7 @@ open Mod_subst
open Misctypes
open Decl_kinds
open Context.Named.Declaration
+open Ltac_pretype
type _ delay =
| Now : 'a delay
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index b70bfd83c1..f03bde68ec 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -15,6 +15,7 @@ open Termops
open Mod_subst
open Misctypes
open Evd
+open Ltac_pretype
type _ delay =
| Now : 'a delay
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cb76df4e8a..0f1a508c8d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -176,6 +176,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
let s = ESorts.kind sigma s in
lookup_canonical_conversion
(proji, Sort_cs (family_of_sort s)),[]
+ | Proj (p, c) ->
+ let c2 = Globnames.ConstRef (Projection.constant p) in
+ let c = Retyping.expand_projection env sigma p c [] in
+ let _, args = destApp sigma c in
+ let sk2 = Stack.append_app args sk2 in
+ lookup_canonical_conversion (proji, Const_cs c2), sk2
| _ ->
let (c2, _) = Termops.global_of_constr sigma t2 in
lookup_canonical_conversion (proji, Const_cs c2),sk2
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ad1409f5b1..7f81d1aa34 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -842,6 +842,15 @@ let rec find_solution_type evarenv = function
| (id,ProjectEvar _)::l -> find_solution_type evarenv l
| [] -> assert false
+let find_most_recent_projection evi sols =
+ let sign = List.map get_id (evar_filtered_context evi) in
+ match sols with
+ | y::l ->
+ List.fold_right (fun (id,p as x) (id',_ as y) ->
+ if List.index Id.equal id sign < List.index Id.equal id' sign then x else y)
+ l y
+ | _ -> assert false
+
(* In case the solution to a projection problem requires the instantiation of
* subsidiary evars, [do_projection_effects] performs them; it
* also try to instantiate the type of those subsidiary evars if their
@@ -1429,7 +1438,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
let c, p = match sols with
| [] -> raise Not_found
| [id,p] -> (mkVar id, p)
- | (id,p)::_::_ ->
+ | _ ->
+ let (id,p) = find_most_recent_projection evi sols in
if choose then (mkVar id, p) else raise (NotUniqueInType sols)
in
let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 7804cc6796..055fd68f6c 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -13,6 +13,7 @@ open Globnames
open Misctypes
open Glob_term
open Evar_kinds
+open Ltac_pretype
(* Untyped intermediate terms, after ASTs and before constr. *)
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 49ea9727c6..f27928662e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob
val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
-val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name
-val empty_lvar : Glob_term.ltac_var_map
+val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name
+val empty_lvar : Ltac_pretype.ltac_var_map
diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml
new file mode 100644
index 0000000000..be8579c2e5
--- /dev/null
+++ b/pretyping/ltac_pretype.ml
@@ -0,0 +1,68 @@
+open Names
+open Glob_term
+
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+ of a matching. Matching can return terms defined in a some context
+ of named binders; in the context, variable names are ordered by
+ (<) and referred to by index in the term Thanks to the canonical
+ ordering, a matching problem like
+
+ [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+ will be accepted. Thanks to the reference by index, a matching
+ problem like
+
+ [match ... with [(fun x => ?p)] => [forall x => p]]
+
+ will work even if [x] is also the name of an existing goal
+ variable.
+
+ Note: we do not keep types in the signature. Besides simplicity,
+ the main reason is that it would force to close the signature over
+ binders that occur only in the types of effective binders but not
+ in the term itself (e.g. for a term [f x] with [f:A -> True] and
+ [x:A]).
+
+ On the opposite side, by not keeping the types, we loose
+ opportunity to propagate type informations which otherwise would
+ not be inferable, as e.g. when matching [forall x, x = 0] with
+ pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+ expression [forall x, h = x] where nothing tells how the type of x
+ could be inferred. We also loose the ability of typing ltac
+ variables before calling the right-hand-side of ltac matching clauses. *)
+
+type constr_under_binders = Id.t list * EConstr.constr
+
+(** Types of substitutions with or w/o bound variables *)
+
+type patvar_map = EConstr.constr Id.Map.t
+type extended_patvar_map = constr_under_binders Id.Map.t
+
+(** A globalised term together with a closure representing the value
+ of its free variables. Intended for use when these variables are taken
+ from the Ltac environment. *)
+type closure = {
+ idents:Id.t Id.Map.t;
+ typed: constr_under_binders Id.Map.t ;
+ untyped:closed_glob_constr Id.Map.t }
+and closed_glob_constr = {
+ closure: closure;
+ term: glob_constr }
+
+(** Ltac variable maps *)
+type var_map = constr_under_binders Id.Map.t
+type uconstr_var_map = closed_glob_constr Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
+
+type ltac_var_map = {
+ ltac_constrs : var_map;
+ (** Ltac variables bound to constrs *)
+ ltac_uconstrs : uconstr_var_map;
+ (** Ltac variables bound to untyped constrs *)
+ ltac_idents: Id.t Id.Map.t;
+ (** Ltac variables bound to identifiers *)
+ ltac_genargs : unbound_ltac_var_map;
+ (** Ltac variables bound to other kinds of arguments *)
+}
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 39c2ceeba8..1038945c18 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -5,13 +5,11 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open CErrors
open Term
open Vars
open Environ
open Reduction
-open Univ
open Declarations
open Names
open Inductive
@@ -20,8 +18,6 @@ open Nativecode
open Nativevalues
open Context.Rel.Declaration
-module RelDecl = Context.Rel.Declaration
-
(** This module implements normalization by evaluation to OCaml code *)
exception Find_at of int
@@ -177,44 +173,6 @@ let build_case_type dep p realargs c =
if dep then mkApp(mkApp(p, realargs), [|c|])
else mkApp(p, realargs)
-(* TODO move this function *)
-let type_of_rel env n =
- env |> lookup_rel n |> RelDecl.get_type |> lift n
-
-let type_of_prop = mkSort type1_sort
-
-let type_of_sort s =
- match s with
- | Prop _ -> type_of_prop
- | Type u -> mkType (Univ.super u)
-
-let type_of_var env id =
- let open Context.Named.Declaration in
- try env |> lookup_named id |> get_type
- with Not_found ->
- anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.")
-
-let sort_of_product env domsort rangsort =
- match (domsort, rangsort) with
- (* Product rule (s,Prop,Prop) *)
- | (_, Prop Null) -> rangsort
- (* Product rule (Prop/Set,Set,Set) *)
- | (Prop _, Prop Pos) -> rangsort
- (* Product rule (Type,Set,?) *)
- | (Type u1, Prop Pos) ->
- if is_impredicative_set env then
- (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
- rangsort
- else
- (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
- Type (sup u1 type0_univ)
- (* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Pos, Type u2) -> Type (sup type0_univ u2)
- (* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Null, Type _) -> rangsort
- (* Product rule (Type_i,Type_i,Type_i) *)
- | (Type u1, Type u2) -> Type (sup u1 u2)
-
(* normalisation of values *)
let branch_of_switch lvl ans bs =
@@ -328,15 +286,15 @@ and nf_atom_type env sigma atom =
match atom with
| Arel i ->
let n = (nb_rel env - i) in
- mkRel n, type_of_rel env n
+ mkRel n, Typeops.type_of_relative env n
| Aconstant cst ->
mkConstU cst, Typeops.type_of_constant_in env cst
| Aind ind ->
mkIndU ind, Inductiveops.type_of_inductive env ind
| Asort s ->
- mkSort s, type_of_sort s
+ mkSort s, Typeops.type_of_sort s
| Avar id ->
- mkVar id, type_of_var env id
+ mkVar id, Typeops.type_of_variable env id
| Acase(ans,accu,p,bs) ->
let a,ta = nf_accu_type env sigma accu in
let ((mind,_),u as ind),allargs = find_rectype_a env ta in
@@ -387,7 +345,7 @@ and nf_atom_type env sigma atom =
let vn = mk_rel_accu (nb_rel env) in
let env = push_rel (LocalAssum (n,dom)) env in
let codom,s2 = nf_type_sort env sigma (codom vn) in
- mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
+ mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
| Aevar(ev,ty) ->
let ty = nf_type env sigma ty in
mkEvar ev, ty
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3b3ad021e4..aaa9467068 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -96,6 +96,31 @@ let rec occur_meta_pattern = function
| PMeta _ | PSoApp _ -> true
| PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
+let rec occurn_pattern n = function
+ | PRel p -> Int.equal n p
+ | PApp (f,args) ->
+ (occurn_pattern n f) || (Array.exists (occurn_pattern n) args)
+ | PProj (_,arg) -> occurn_pattern n arg
+ | PLambda (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+ | PProd (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+ | PLetIn (na,b,t,c) ->
+ Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t ||
+ (occurn_pattern (n+1) c)
+ | PIf (c,c1,c2) ->
+ (occurn_pattern n c) ||
+ (occurn_pattern n c1) || (occurn_pattern n c2)
+ | PCase(_,p,c,br) ->
+ (occurn_pattern n p) ||
+ (occurn_pattern n c) ||
+ (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
+ | PMeta _ | PSoApp _ -> true
+ | PEvar (_,args) -> Array.exists (occurn_pattern n) args
+ | PVar _ | PRef _ | PSort _ -> false
+ | PFix fix -> not (noccurn n (mkFix fix))
+ | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+
+let noccurn_pattern n c = not (occurn_pattern n c)
+
exception BoundPattern;;
let rec head_pattern_bound t =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 3a1faf1c77..2d1ce1dbc9 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -12,6 +12,7 @@ open Glob_term
open Mod_subst
open Misctypes
open Pattern
+open Ltac_pretype
(** {5 Functions on patterns} *)
@@ -21,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool
val subst_pattern : substitution -> constr_pattern -> constr_pattern
+val noccurn_pattern : int -> constr_pattern -> bool
+
exception BoundPattern
(** [head_pattern_bound t] extracts the head variable/constant of the
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ea1f2de539..30783bfad5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -43,6 +43,7 @@ open Glob_term
open Glob_ops
open Evarconv
open Misctypes
+open Ltac_pretype
module NamedDecl = Context.Named.Declaration
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 5822f5add5..6537d1ecf7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,6 +18,7 @@ open Evd
open EConstr
open Glob_term
open Evarutil
+open Ltac_pretype
(** An auxiliary function for searching for fixpoint guard indexes *)
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index d04dcb8e3b..9904b73540 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,3 +1,4 @@
+Ltac_pretype
Locusops
Pretype_errors
Reductionops
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index a23579609a..e970a1db90 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -171,7 +171,7 @@ let keep_true_projections projs kinds =
let filter (p, (_, b)) = if b then Some p else None in
List.map_filter filter (List.combine projs kinds)
-let cs_pattern_of_constr t =
+let cs_pattern_of_constr env t =
match kind_of_term t with
App (f,vargs) ->
begin
@@ -180,6 +180,10 @@ let cs_pattern_of_constr t =
end
| Rel n -> Default_cs, Some n, []
| Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
+ | Proj (p, c) ->
+ let { Environ.uj_type = ty } = Typeops.infer env c in
+ let _, params = Inductive.find_rectype env ty in
+ Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
| Sort s -> Sort_cs (family_of_sort s), None, []
| _ ->
begin
@@ -190,7 +194,6 @@ let cs_pattern_of_constr t =
let warn_projection_no_head_constant =
CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
(fun (sign,env,t,con,proji_sp) ->
- let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
let env = Termops.push_rels_assum sign env in
let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
@@ -207,14 +210,16 @@ let compute_canonical_projections warn (con,ind) =
let v = (mkConstU (con,u)) in
let c = Environ.constant_value_in env (con,u) in
let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+ let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
let t = EConstr.Unsafe.to_constr t in
- let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in
+ let lt = List.rev_map snd sign in
let args = snd (decompose_app t) in
let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
lookup_structure ind in
let params, projs = List.chop p args in
let lpj = keep_true_projections lpj kl in
let lps = List.combine lpj projs in
+ let nenv = Termops.push_rels_assum sign env in
let comp =
List.fold_left
(fun l (spopt,t) -> (* comp=components *)
@@ -222,7 +227,7 @@ let compute_canonical_projections warn (con,ind) =
| Some proji_sp ->
begin
try
- let patt, n , args = cs_pattern_of_constr t in
+ let patt, n , args = cs_pattern_of_constr nenv t in
((ConstRef proji_sp, patt, t, n, args) :: l)
with Not_found ->
if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);
@@ -324,15 +329,25 @@ let declare_canonical_structure ref =
let lookup_canonical_conversion (proj,pat) =
assoc_pat pat (Refmap.find proj !object_table)
+let decompose_projection sigma c args =
+ match EConstr.kind sigma c with
+ | Const (c, u) ->
+ let n = find_projection_nparams (ConstRef c) in
+ (** Check if there is some canonical projection attached to this structure *)
+ let _ = Refmap.find (ConstRef c) !object_table in
+ let arg = Stack.nth args n in
+ arg
+ | Proj (p, c) ->
+ let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in
+ c
+ | _ -> raise Not_found
+
let is_open_canonical_projection env sigma (c,args) =
let open EConstr in
try
- let (ref, _) = Termops.global_of_constr sigma c in
- let n = find_projection_nparams ref in
- (** Check if there is some canonical projection attached to this structure *)
- let _ = Refmap.find ref !object_table in
+ let arg = decompose_projection sigma c args in
try
- let arg = whd_all env sigma (Stack.nth args n) in
+ let arg = whd_all env sigma arg in
let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
not (isConstruct sigma hd)
with Failure _ -> false
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5480b14af0..8e2333b349 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -65,7 +65,7 @@ type obj_typ = {
o_TCOMPS : constr list } (** ordered *)
(** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
+val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list
val pr_cs_pattern : cs_pattern -> Pp.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 079524f344..56f8b33e01 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -214,7 +214,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty
| Const (cst, u) ->
let t = constant_type_in env (cst, EInstance.kind sigma u) in
- (* TODO *)
sigma, EConstr.of_constr t
| Var id -> sigma, type_of_var env id
| Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 91726e8c6d..a6b8262f7f 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -15,6 +15,7 @@ open Pattern
open Globnames
open Locus
open Univ
+open Ltac_pretype
type reduction_tactic_error =
InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d52c3932df..e8f7e2bbaf 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -501,6 +501,10 @@ let expand_key ts env sigma = function
in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red
| None -> None
+let isApp_or_Proj sigma c =
+ match kind sigma c with
+ | App _ | Proj _ -> true
+ | _ -> false
type unirec_flags = {
at_top: bool;
@@ -1020,7 +1024,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
let f1 () =
- if isApp sigma cM then
+ if isApp_or_Proj sigma cM then
let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
if is_open_canonical_projection curenv sigma f1l1 then
let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
@@ -1036,7 +1040,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else
try f1 () with e when precatchable_exception e ->
- if isApp sigma cN then
+ if isApp_or_Proj sigma cN then
let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
if is_open_canonical_projection curenv sigma f2l2 then
let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 20:59:51 +0000