aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/indtypes.ml7
-rw-r--r--checker/inductive.ml2
-rw-r--r--clib/cArray.ml12
-rw-r--r--clib/cArray.mli2
-rw-r--r--clib/cMap.ml26
-rw-r--r--clib/cMap.mli6
-rw-r--r--clib/hMap.ml4
-rw-r--r--default.nix21
-rw-r--r--kernel/environ.ml42
-rw-r--r--kernel/environ.mli5
-rw-r--r--kernel/reduction.ml81
-rw-r--r--kernel/typeops.ml3
-rw-r--r--kernel/typeops.mli3
-rw-r--r--library/libobject.ml2
-rw-r--r--library/nametab.ml20
-rw-r--r--library/nametab.mli7
-rw-r--r--pretyping/arguments_renaming.mli2
-rw-r--r--pretyping/inductiveops.ml5
-rw-r--r--pretyping/typing.ml58
-rw-r--r--pretyping/typing.mli2
-rw-r--r--tactics/tactics.ml17
-rw-r--r--test-suite/coqchk/bug_8655.v1
-rw-r--r--test-suite/coqchk/bug_8881.v23
-rw-r--r--test-suite/success/Inductive.v2
24 files changed, 246 insertions, 107 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 50e65ef587..f6c510ee1c 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -531,10 +531,11 @@ let check_positivity env_ar mind params nrecp inds =
Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
let lra_ind = List.rev (Array.to_list rc) in
let lparams = rel_context_length params in
+ let ra_env =
+ List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
+ let env_ar_par = push_rel_context params env_ar in
let check_one i mip =
- let ra_env =
- List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
- let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
+ let ienv = (env_ar_par, 1+lparams, ntypes, ra_env) in
check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
let irecargs = Array.mapi check_one inds in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 5e34f04f51..269a98cb0e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -388,7 +388,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
let check_case_info env indsp ci =
let mib, mip as spec = lookup_mind_specif env indsp in
if
- not (eq_ind_chk indsp ci.ci_ind) ||
+ not (mind_equiv env indsp ci.ci_ind) ||
(mib.mind_nparams <> ci.ci_npar) ||
(mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
(mip.mind_consnrealargs <> ci.ci_cstr_nargs) ||
diff --git a/clib/cArray.ml b/clib/cArray.ml
index 9644834381..c3a693ff16 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -35,6 +35,8 @@ sig
val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
val fold_right2 :
('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
+ val fold_right3 :
+ ('a -> 'b -> 'c -> 'd -> 'd) -> 'a array -> 'b array -> 'c array -> 'd -> 'd
val fold_left2 :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left3 :
@@ -252,6 +254,16 @@ let fold_left2_i f a v1 v2 =
if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i";
fold a 0
+let fold_right3 f v1 v2 v3 a =
+ let lv1 = Array.length v1 in
+ let rec fold a n =
+ if n=0 then a
+ else
+ let k = n-1 in
+ fold (f (uget v1 k) (uget v2 k) (uget v3 k) a) k in
+ if Array.length v2 <> lv1 || Array.length v3 <> lv1 then invalid_arg "Array.fold_right3";
+ fold a lv1
+
let fold_left3 f a v1 v2 v3 =
let lv1 = Array.length v1 in
let rec fold a n =
diff --git a/clib/cArray.mli b/clib/cArray.mli
index e65a56d15e..21479d2b45 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -58,6 +58,8 @@ sig
val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
val fold_right2 :
('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
+ val fold_right3 :
+ ('a -> 'b -> 'c -> 'd -> 'd) -> 'a array -> 'b array -> 'c array -> 'd -> 'd
val fold_left2 :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left3 :
diff --git a/clib/cMap.ml b/clib/cMap.ml
index 040dede0a2..e4ce6c7c02 100644
--- a/clib/cMap.ml
+++ b/clib/cMap.ml
@@ -35,6 +35,7 @@ sig
val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val height : 'a t -> int
+ val filter_range : (key -> int) -> 'a t -> 'a t
module Smart :
sig
val map : ('a -> 'a) -> 'a t -> 'a t
@@ -62,6 +63,7 @@ sig
val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val height : 'a map -> int
+ val filter_range : (M.t -> int) -> 'a map -> 'a map
module Smart :
sig
val map : ('a -> 'a) -> 'a map -> 'a map
@@ -85,8 +87,11 @@ struct
if this happens, we can still implement a less clever version of [domain].
*)
- type 'a map = 'a Map.Make(M).t
- type set = Set.Make(M).t
+ module F = Map.Make(M)
+ type 'a map = 'a F.t
+
+ module S = Set.Make(M)
+ type set = S.t
type 'a _map =
| MEmpty
@@ -164,6 +169,23 @@ struct
| MEmpty -> 0
| MNode (_, _, _, _, h) -> h
+ (* Filter based on a range *)
+ let filter_range in_range m =
+ let rec aux m = function
+ | MEmpty -> m
+ | MNode (l, k, v, r, _) ->
+ let vr = in_range k in
+ (* the range is below the current value *)
+ if vr < 0 then aux m (map_prj l)
+ (* the range is above the current value *)
+ else if vr > 0 then aux m (map_prj r)
+ (* The current value is in the range *)
+ else
+ let m = aux m (map_prj l) in
+ let m = aux m (map_prj r) in
+ F.add k v m
+ in aux F.empty (map_prj m)
+
module Smart =
struct
diff --git a/clib/cMap.mli b/clib/cMap.mli
index f5496239f6..ca6ddb2f4e 100644
--- a/clib/cMap.mli
+++ b/clib/cMap.mli
@@ -60,6 +60,12 @@ sig
val height : 'a t -> int
(** An indication of the logarithmic size of a map *)
+ val filter_range : (key -> int) -> 'a t -> 'a t
+ (** [find_range in_range m] Given a comparison function [in_range x],
+ that tests if [x] is below, above, or inside a given range
+ [filter_range] returns the submap of [m] whose keys are in
+ range. Note that [in_range] has to define a continouous range. *)
+
module Smart :
sig
val map : ('a -> 'a) -> 'a t -> 'a t
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 33cb6d0131..9c80398e4d 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -398,6 +398,10 @@ struct
let height s = Int.Map.height s
+ (* Not as efficient as the original version *)
+ let filter_range f s =
+ filter (fun x _ -> f x = 0) s
+
module Unsafe =
struct
let map f s =
diff --git a/default.nix b/default.nix
index 9a7afbe89e..7c8113c9ab 100644
--- a/default.nix
+++ b/default.nix
@@ -23,8 +23,8 @@
{ pkgs ?
(import (fetchTarball {
- url = "https://github.com/NixOS/nixpkgs/archive/06613c189eebf4d6167d2d010a59cf38b43b6ff4.tar.gz";
- sha256 = "13grhy3cvdwr7wql1rm5d7zsfpvp44cyjhiain4zs70r90q3swdg";
+ url = "https://github.com/NixOS/nixpkgs/archive/69522a0acf8e840e8b6ac0a9752a034ab74eb3c0.tar.gz";
+ sha256 = "12k80gd4lkw9h9y1szvmh0jmh055g3b6wnphmx4ab1qdwlfaylnx";
}) {})
, ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06
, buildIde ? true
@@ -33,6 +33,7 @@
, shell ? false
# We don't use lib.inNixShell because that would also apply
# when in a nix-shell of some package depending on this one.
+, coq-version ? "8.10-git"
}:
with pkgs;
@@ -101,7 +102,20 @@ stdenv.mkDerivation rec {
installCheckTarget = [ "check" ];
- passthru = { inherit ocamlPackages; };
+ passthru = {
+ inherit coq-version ocamlPackages;
+ dontFilter = true; # Useful to use mkCoqPackages from <nixpkgs>
+ };
+
+ setupHook = writeText "setupHook.sh" "
+ addCoqPath () {
+ if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then
+ export COQPATH=\"$COQPATH\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\"
+ fi
+ }
+
+ addEnvHooks \"$targetOffset\" addCoqPath
+ ";
meta = {
description = "Coq proof assistant";
@@ -113,6 +127,7 @@ stdenv.mkDerivation rec {
'';
homepage = http://coq.inria.fr;
license = licenses.lgpl21;
+ platforms = platforms.unix;
};
}
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e341412294..f61dd0c101 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -350,9 +350,6 @@ let map_universes f env =
{ env with env_stratification =
{ s with env_universes = f s.env_universes } }
-let set_universes env u =
- { env with env_stratification = { env.env_stratification with env_universes = u } }
-
let add_constraints c env =
if Univ.Constraint.is_empty c then env
else map_universes (UGraph.merge_constraints c) env
@@ -405,19 +402,12 @@ let add_constant_key kn cb linkinfo env =
let add_constant kn cb env =
add_constant_key kn cb no_link_info env
-let constraints_of cb u =
- match cb.const_universes with
- | Monomorphic_const _ -> Univ.Constraint.empty
- | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
-
(* constant_type gives the type of a constant *)
let constant_type env (kn,u) =
let cb = lookup_constant kn env in
- match cb.const_universes with
- | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
- | Polymorphic_const _ctx ->
- let csts = constraints_of cb u in
- (subst_instance_constr u cb.const_type, csts)
+ let uctx = Declareops.constant_polymorphic_context cb in
+ let csts = Univ.AUContext.instantiate u uctx in
+ (subst_instance_constr u cb.const_type, csts)
type const_evaluation_result = NoBody | Opaque
@@ -425,20 +415,14 @@ exception NotEvaluableConst of const_evaluation_result
let constant_value_and_type env (kn, u) =
let cb = lookup_constant kn env in
- if Declareops.constant_is_polymorphic cb then
- let cst = constraints_of cb u in
- let b' = match cb.const_body with
- | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
- | OpaqueDef _ -> None
- | Undef _ -> None
- in
- b', subst_instance_constr u cb.const_type, cst
- else
- let b' = match cb.const_body with
- | Def l_body -> Some (Mod_subst.force_constr l_body)
- | OpaqueDef _ -> None
- | Undef _ -> None
- in b', cb.const_type, Univ.Constraint.empty
+ let uctx = Declareops.constant_polymorphic_context cb in
+ let cst = Univ.AUContext.instantiate u uctx in
+ let b' = match cb.const_body with
+ | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
+ | OpaqueDef _ -> None
+ | Undef _ -> None
+ in
+ b', subst_instance_constr u cb.const_type, cst
let body_of_constant_body env cb =
let otab = opaque_tables env in
@@ -457,9 +441,7 @@ let body_of_constant_body env cb =
(* constant_type gives the type of a constant *)
let constant_type_in env (kn,u) =
let cb = lookup_constant kn env in
- if Declareops.constant_is_polymorphic cb then
- subst_instance_constr u cb.const_type
- else cb.const_type
+ subst_instance_constr u cb.const_type
let constant_value_in env (kn,u) =
let cb = lookup_constant kn env in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0255581749..c285f907fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -155,11 +155,6 @@ val named_body : variable -> env -> constr option
val fold_named_context :
(env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
-val set_universes : env -> UGraph.t -> env
-(** This is used to update universes during a proof for the sake of
- evar map-unaware functions, eg [Typing] calling
- [Typeops.check_hyps_inclusion]. *)
-
(** Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse :
('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 18697d07e5..5515ff9767 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -68,7 +68,7 @@ type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
| Zlproj of Projection.Repr.t * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
- | Zlcase of case_info * lift * fconstr * fconstr array
+ | Zlcase of case_info * lift * constr * constr array * fconstr subs
and lft_constr_stack = lft_constr_stack_elt list
let rec zlapp v = function
@@ -102,7 +102,7 @@ let pure_stack lfts stk =
let (lfx,pa) = pure_rec l a in
(l, Zlfix((lfx,fx),pa)::pstk)
| (ZcaseT(ci,p,br,e),(l,pstk)) ->
- (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk))
+ (l,Zlcase(ci,l,p,br,e)::pstk))
in
snd (pure_rec lfts stk)
@@ -288,31 +288,13 @@ let conv_table_key infos k1 k2 cuniv =
| RelKey n, RelKey n' when Int.equal n n' -> cuniv
| _ -> raise NotConvertible
-let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
- let rec cmp_rec pstk1 pstk2 cuniv =
- match (pstk1,pstk2) with
- | (z1::s1, z2::s2) ->
- let cu1 = cmp_rec s1 s2 cuniv in
- (match (z1,z2) with
- | (Zlapp a1,Zlapp a2) ->
- Array.fold_right2 f a1 a2 cu1
- | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
- if not (Projection.Repr.equal c1 c2) then
- raise NotConvertible
- else cu1
- | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
- let cu2 = f fx1 fx2 cu1 in
- cmp_rec a1 a2 cu2
- | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
- if not (fmind ci1.ci_ind ci2.ci_ind) then
- raise NotConvertible;
- let cu2 = f (l1,p1) (l2,p2) cu1 in
- Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2
- | _ -> assert false)
- | _ -> cuniv in
- if compare_stack_shape stk1 stk2 then
- cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
- else raise NotConvertible
+exception IrregularPatternShape
+
+let rec skip_pattern n c =
+ if Int.equal n 0 then c
+ else match kind c with
+ | Lambda (_, _, c) -> skip_pattern (pred n) c
+ | _ -> raise IrregularPatternShape
type conv_tab = {
cnv_inf : clos_infos;
@@ -611,10 +593,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| FProd _ | FEvar _), _ -> raise NotConvertible
and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
- compare_stacks
- (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
- (eq_ind)
- lft1 stk1 lft2 stk2 cuniv
+ let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in
+ let rec cmp_rec pstk1 pstk2 cuniv =
+ match (pstk1,pstk2) with
+ | (z1::s1, z2::s2) ->
+ let cu1 = cmp_rec s1 s2 cuniv in
+ (match (z1,z2) with
+ | (Zlapp a1,Zlapp a2) ->
+ Array.fold_right2 f a1 a2 cu1
+ | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
+ if not (Projection.Repr.equal c1 c2) then
+ raise NotConvertible
+ else cu1
+ | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
+ let cu2 = f fx1 fx2 cu1 in
+ cmp_rec a1 a2 cu2
+ | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
+ if not (eq_ind ci1.ci_ind ci2.ci_ind) then
+ raise NotConvertible;
+ let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
+ convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
+ | _ -> assert false)
+ | _ -> cuniv in
+ if compare_stack_shape stk1 stk2 then
+ cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
+ else raise NotConvertible
and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let lv1 = Array.length v1 in
@@ -629,6 +632,22 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
fold 0 cuniv
else raise NotConvertible
+and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
+ (** Skip comparison of the pattern types. We know that the two terms are
+ living in a common type, thus this check is useless. *)
+ let fold n c1 c2 cuniv = match skip_pattern n c1, skip_pattern n c2 with
+ | (c1, c2) ->
+ let lft1 = el_liftn n lft1 in
+ let lft2 = el_liftn n lft2 in
+ let e1 = subs_liftn n e1 in
+ let e2 = subs_liftn n e2 in
+ ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+ | exception IrregularPatternShape ->
+ (** Might happen due to a shape invariant that is not enforced *)
+ ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+ in
+ Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
+
let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
let infos = create_clos_infos ~evars reds env in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1bb2d3c79c..c8fd83c8a9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -91,7 +91,8 @@ let type_of_variable env id =
(* Checks if a context of variables can be instantiated by the
variables of the current env.
Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env f c sign =
+let check_hyps_inclusion env ?evars f c sign =
+ let conv env a b = conv env ?evars a b in
Context.Named.fold_outside
(fun d1 () ->
let open Context.Named.Declaration in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d24002065b..4193324136 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -116,4 +116,5 @@ val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit
+val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+ ('a -> constr) -> 'a -> Constr.named_context -> unit
diff --git a/library/libobject.ml b/library/libobject.ml
index ea19fbb90b..43934304c2 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -71,7 +71,7 @@ type dynamic_object_declaration = {
let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
let cache_tab =
- (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
+ (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t)
let declare_object_full odecl =
let na = odecl.object_name in
diff --git a/library/nametab.ml b/library/nametab.ml
index 06ace373c3..029d850504 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -74,6 +74,8 @@ module type NAMETREE = sig
val user_name : qualid -> t -> user_name
val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
val find_prefixes : qualid -> t -> elt list
+ (** Matches a prefix of [qualid], useful for completion *)
+ val match_prefixes : qualid -> t -> elt list
end
module Make (U : UserName) (E : EqualityType) : NAMETREE
@@ -259,9 +261,19 @@ let find_prefixes qid tab =
search_prefixes (Id.Map.find id tab) (DirPath.repr dir)
with Not_found -> []
-end
-
+let match_prefixes =
+ let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in
+ fun qid tab ->
+ try
+ let (dir,id) = repr_qualid qid in
+ let id_prefix = cprefix Id.(to_string id) in
+ let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in
+ let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in
+ (* Coq's flatten is "magical", so this is not so bad perf-wise *)
+ CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches [])
+ with Not_found -> []
+end
(* Global name tables *************************************************)
@@ -447,6 +459,10 @@ let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab
let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab
+(* Completion *)
+let completion_canditates qualid =
+ ExtRefTab.match_prefixes qualid !the_ccitab
+
(* Derived functions *)
let locate_constant qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index 1c3322bfb1..1e479b200b 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -118,6 +118,12 @@ val locate_extended_all : qualid -> extended_global_reference list
val locate_extended_all_dir : qualid -> global_dir_reference list
val locate_extended_all_modtype : qualid -> ModPath.t list
+(** Experimental completion support, API is _unstable_ *)
+val completion_canditates : qualid -> extended_global_reference list
+(** [completion_canditates qualid] will return the list of global
+ references that have [qualid] as a prefix. UI usually will want to
+ compose this with [shortest_qualid_of_global] *)
+
(** Mapping a full path to a global reference *)
val global_of_path : full_path -> GlobRef.t
@@ -211,6 +217,7 @@ module type NAMETREE = sig
val user_name : qualid -> t -> user_name
val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
val find_prefixes : qualid -> t -> elt list
+ val match_prefixes : qualid -> t -> elt list
end
module Make (U : UserName) (E : EqualityType) :
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index 6a776dc961..6d1b6eefd4 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -17,6 +17,8 @@ val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit
(** [Not_found] is raised if no names are defined for [r] *)
val arguments_names : GlobRef.t -> Name.t list
+val rename_type : types -> GlobRef.t -> types
+
val rename_type_of_constant : env -> pconstant -> types
val rename_type_of_inductive : env -> pinductive -> types
val rename_type_of_constructor : env -> pconstructor -> types
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ea222397a8..14358dd02a 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -746,8 +746,11 @@ let type_of_projection_knowing_arg env sigma p c ty =
syntactic conditions *)
let control_only_guard env sigma c =
+ let c = Evarutil.nf_evar sigma c in
let check_fix_cofix e c =
- match kind (EConstr.to_constr sigma c) with
+ (** [c] has already been normalized upfront *)
+ let c = EConstr.Unsafe.to_constr c in
+ match kind c with
| CoFix (_,(_,_,_) as cofix) ->
Inductive.check_cofix e cofix
| Fix (_,(_,_,_) as fix) ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index dc3f042431..b5729d7574 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -218,9 +218,6 @@ let judge_of_cast env sigma cj k tj =
sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
uj_type = expected_type }
-let enrich_env env sigma =
- set_universes env @@ Evd.universes sigma
-
let check_fix env sigma pfix =
let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let (idx, (ids, cs, ts)) = pfix in
@@ -277,6 +274,38 @@ let judge_of_letin env name defj typj j =
{ uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
uj_type = subst1 defj.uj_val j.uj_type }
+let check_hyps_inclusion env sigma f x hyps =
+ let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
+ let f x = EConstr.Unsafe.to_constr (f x) in
+ Typeops.check_hyps_inclusion env ~evars f x hyps
+
+let type_of_constant env sigma (c,u) =
+ let open Declarations in
+ let cb = Environ.lookup_constant c env in
+ let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in
+ let u = EInstance.kind sigma u in
+ let ty, csts = Environ.constant_type env (c,u) in
+ let sigma = Evd.add_constraints sigma csts in
+ sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c)))
+
+let type_of_inductive env sigma (ind,u) =
+ let open Declarations in
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let u = EInstance.kind sigma u in
+ let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
+ let sigma = Evd.add_constraints sigma csts in
+ sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind)))
+
+let type_of_constructor env sigma ((ind,_ as ctor),u) =
+ let open Declarations in
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let u = EInstance.kind sigma u in
+ let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in
+ let sigma = Evd.add_constraints sigma csts in
+ sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
+
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
let rec execute env sigma cstr =
@@ -297,17 +326,17 @@ let rec execute env sigma cstr =
| Var id ->
sigma, judge_of_variable env id
- | Const (c, u) ->
- let u = EInstance.kind sigma u in
- sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
+ | Const c ->
+ let sigma, ty = type_of_constant env sigma c in
+ sigma, make_judge cstr ty
- | Ind (ind, u) ->
- let u = EInstance.kind sigma u in
- sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
+ | Ind ind ->
+ let sigma, ty = type_of_inductive env sigma ind in
+ sigma, make_judge cstr ty
- | Construct (cstruct, u) ->
- let u = EInstance.kind sigma u in
- sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
+ | Construct ctor ->
+ let sigma, ty = type_of_constructor env sigma ctor in
+ sigma, make_judge cstr ty
| Case (ci,p,c,lf) ->
let sigma, cj = execute env sigma c in
@@ -391,7 +420,6 @@ and execute_recdef env sigma (names,lar,vdef) =
and execute_array env = Array.fold_left_map (execute env)
let check env sigma c t =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
match Evarconv.cumul env sigma j.uj_type t with
| None ->
@@ -401,14 +429,12 @@ let check env sigma c t =
(* Type of a constr *)
let unsafe_type_of env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
j.uj_type
(* Sort of a type *)
let sort_of env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
let sigma, a = type_judgment env sigma j in
sigma, a.utj_type
@@ -416,7 +442,6 @@ let sort_of env sigma c =
(* Try to solve the existential variables by typing *)
let type_of ?(refresh=false) env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
(* side-effect on evdref *)
if refresh then
@@ -424,7 +449,6 @@ let type_of ?(refresh=false) env sigma c =
else sigma, j.uj_type
let solve_evars env sigma c =
- let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
(* side-effect on evdref *)
sigma, nf_evar sigma j.uj_val
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index b8830ff4a2..366af0772f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -48,6 +48,8 @@ val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ->
val judge_of_prop : unsafe_judgment
val judge_of_set : unsafe_judgment
+val judge_of_apply : env -> evar_map -> unsafe_judgment -> unsafe_judgment array ->
+ evar_map * unsafe_judgment
val judge_of_abstraction : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
val judge_of_product : Environ.env -> Name.t ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25f9bc5576..5cead11a5c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4097,12 +4097,15 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
let guess_elim isrec dep s hyp0 gl =
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
- let evd, elimc =
- if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl
+ let env = Tacmach.New.pf_env gl in
+ let sigma = Tacmach.New.project gl in
+ let sigma, elimc =
+ if isrec && not (is_nonrec mind)
+ then
+ let gr = lookup_eliminator mind s in
+ Evd.fresh_global env sigma gr
else
- let env = Tacmach.New.pf_env gl in
- let sigma = Tacmach.New.project gl in
- let u = EInstance.kind (Tacmach.New.project gl) u in
+ let u = EInstance.kind sigma u in
if dep then
let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
let ind = EConstr.of_constr ind in
@@ -4112,8 +4115,8 @@ let guess_elim isrec dep s hyp0 gl =
let ind = EConstr.of_constr ind in
(sigma, ind)
in
- let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
- evd, ((elimc, NoBindings), elimt), mkIndU (mind, u)
+ let elimt = Typing.unsafe_type_of env sigma elimc in
+ sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
let given_elim hyp0 (elimc,lbind as e) gl =
let sigma = Tacmach.New.project gl in
diff --git a/test-suite/coqchk/bug_8655.v b/test-suite/coqchk/bug_8655.v
new file mode 100644
index 0000000000..06d08b2082
--- /dev/null
+++ b/test-suite/coqchk/bug_8655.v
@@ -0,0 +1 @@
+Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
diff --git a/test-suite/coqchk/bug_8881.v b/test-suite/coqchk/bug_8881.v
new file mode 100644
index 0000000000..dfc209b318
--- /dev/null
+++ b/test-suite/coqchk/bug_8881.v
@@ -0,0 +1,23 @@
+
+(* Check use of equivalence on inductive types (bug #1242) *)
+
+Module Type ASIG.
+ Inductive t : Set := a | b : t.
+ Definition f := fun x => match x with a => true | b => false end.
+End ASIG.
+
+Module Type BSIG.
+ Declare Module A : ASIG.
+ Definition f := fun x => match x with A.a => true | A.b => false end.
+End BSIG.
+
+Module C (A : ASIG) (B : BSIG with Module A:=A).
+
+ (* Check equivalence is considered in "case_info" *)
+ Lemma test : forall x, A.f x = B.f x.
+ Proof.
+ intro x. unfold B.f, A.f.
+ destruct x; reflexivity.
+ Qed.
+
+End C.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index f07c0191f1..c2130995fc 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,7 +1,5 @@
(* Test des definitions inductives imbriquees *)
-Require Import List.
-
Inductive X : Set :=
cons1 : list X -> X.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:31:23 +0000