aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/stdlib/index-list.html.template1
-rw-r--r--interp/constrintern.ml16
-rw-r--r--pretyping/cases.ml12
-rw-r--r--pretyping/indrec.ml34
-rw-r--r--pretyping/indrec.mli7
-rw-r--r--pretyping/inductiveops.ml34
-rw-r--r--pretyping/inductiveops.mli15
-rw-r--r--printing/prettyp.ml8
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--tactics/elimschemes.mli2
-rw-r--r--tactics/equality.ml2
-rw-r--r--test-suite/bugs/closed/4622.v24
-rw-r--r--test-suite/bugs/closed/4873.v72
-rw-r--r--test-suite/success/primitiveproj.v2
-rw-r--r--theories/Compat/Coq85.v4
-rw-r--r--theories/Compat/Coq86.v9
-rw-r--r--theories/Compat/vo.itarget1
-rw-r--r--toplevel/coqinit.ml3
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/himsg.ml7
-rw-r--r--toplevel/indschemes.ml20
-rw-r--r--toplevel/obligations.ml13
22 files changed, 234 insertions, 57 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index fb45777e7..9216c81fc 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -616,5 +616,6 @@ through the <tt>Require Import</tt> command.</p>
theories/Compat/AdmitAxiom.v
theories/Compat/Coq84.v
theories/Compat/Coq85.v
+ theories/Compat/Coq86.v
</dd>
</dl>
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 270109e52..438aa2f7c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1614,11 +1614,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
(merge_impargs l args) loc
| CRecord (loc, fs) ->
- let fields =
- sort_fields ~complete:true loc fs
- (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None))
- in
- begin
+ let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+ let fields =
+ sort_fields ~complete:true loc fs
+ (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st),
+ Misctypes.IntroAnonymous, None))
+ in
+ begin
match fields with
| None -> user_err_loc (loc, "intern", str"No constructor inference.")
| Some (n, constrname, args) ->
@@ -1688,7 +1690,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
GIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole (loc, k, naming, solve) ->
let k = match k with
- | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true)
+ | None ->
+ let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+ Evar_kinds.QuestionMark st
| Some k -> k
in
let solve = match solve with
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 985ad4b0d..447a4c487 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1329,14 +1329,6 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
*)
-let mk_case pb (ci,pred,c,brs) =
- let mib = lookup_mind (fst ci.ci_ind) pb.env in
- match mib.mind_record with
- | Some (Some (_, cs, pbs)) ->
- Reduction.beta_appvect brs.(0)
- (Array.map (fun p -> mkProj (Projection.make p true, c)) cs)
- | _ -> mkCase (ci,pred,c,brs)
-
(**********************************************************************)
(* Main compiling descent *)
let rec compile pb =
@@ -1383,7 +1375,9 @@ and match_current pb (initial,tomatch) =
pred current indt (names,dep) tomatch in
let ci = make_case_info pb.env (fst mind) pb.casestyle in
let pred = nf_betaiota !(pb.evdref) pred in
- let case = mk_case pb (ci,pred,current,brvals) in
+ let case =
+ make_case_or_project pb.env indf ci pred current brvals
+ in
Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
{ uj_val = applist (case, inst);
uj_type = prod_applist typ inst }
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0c80bd019..39aeb41f7 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -36,12 +36,14 @@ type dep_flag = bool
type recursion_scheme_error =
| NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
| NotMutualInScheme of inductive * inductive
+ | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
exception RecursionSchemeError of recursion_scheme_error
let make_prod_dep dep env = if dep then mkProd_name env else mkProd
let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
+
(*******************************************)
(* Building curryfied elimination *)
(*******************************************)
@@ -375,27 +377,9 @@ let mis_make_indrec env sigma listdepkind mib u =
(Anonymous,depind',concl))
arsign'
in
- let obj =
- let projs = get_projections env indf in
- match projs with
- | None -> (mkCase (ci, pred,
- mkRel 1,
- branches))
- | Some ps ->
- let branch = branches.(0) in
- let ctx, br = decompose_lam_assum branch in
- let n, subst =
- List.fold_right (fun decl (i, subst) ->
- match decl with
- | LocalAssum (na,t) ->
- let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
- i + 1, t :: subst
- | LocalDef (na,b,t) ->
- i, mkRel 0 :: subst)
- ctx (0, [])
- in
- let term = substl subst br in
- term
+ let obj =
+ Inductiveops.make_case_or_project env indf ci pred
+ (mkRel 1) branches
in
it_mkLambda_or_LetIn_name env obj
(Termops.lift_rel_context nrec deparsign)
@@ -483,6 +467,8 @@ let mis_make_indrec env sigma listdepkind mib u =
let build_case_analysis_scheme env sigma pity dep kind =
let (mib,mip) = lookup_mind_specif env (fst pity) in
+ if dep && not (Inductiveops.has_dependent_elim mib) then
+ raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity)));
mis_make_case_com dep env sigma pity (mib,mip) kind
let is_in_prop mip =
@@ -492,7 +478,7 @@ let is_in_prop mip =
let build_case_analysis_scheme_default env sigma pity kind =
let (mib,mip) = lookup_mind_specif env (fst pity) in
- let dep = not (is_in_prop mip) in
+ let dep = not (is_in_prop mip || not (Inductiveops.has_dependent_elim mib)) in
mis_make_case_com dep env sigma pity (mib,mip) kind
(**********************************************************************)
@@ -553,6 +539,8 @@ let check_arities env listdepkind =
let build_mutual_induction_scheme env sigma = function
| ((mind,u),dep,s)::lrecspec ->
let (mib,mip) = lookup_mind_specif env mind in
+ if dep && not (Inductiveops.has_dependent_elim mib) then
+ raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind)));
let (sp,tyi) = mind in
let listdepkind =
((mind,u),mib,mip,dep,s)::
@@ -572,6 +560,8 @@ let build_mutual_induction_scheme env sigma = function
let build_induction_scheme env sigma pind dep kind =
let (mib,mip) = lookup_mind_specif env (fst pind) in
+ if dep && not (Inductiveops.has_dependent_elim mib) then
+ raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind)));
let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
sigma, List.hd l
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index f0736d2dd..192b64a5e 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -16,6 +16,7 @@ open Evd
type recursion_scheme_error =
| NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
| NotMutualInScheme of inductive * inductive
+ | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
exception RecursionSchemeError of recursion_scheme_error
@@ -28,13 +29,15 @@ type dep_flag = bool
val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
-(** Build a dependent case elimination predicate unless type is in Prop *)
+(** Build a dependent case elimination predicate unless type is in Prop
+ or is a recursive record with primitive projections. *)
val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
sorts_family -> (constr, 'r) Sigma.sigma
(** Builds a recursive induction scheme (Peano-induction style) in the same
- sort family as the inductive family; it is dependent if not in Prop *)
+ sort family as the inductive family; it is dependent if not in Prop
+ or a recursive record with primitive projections. *)
val build_induction_scheme : env -> evar_map -> pinductive ->
dep_flag -> sorts_family -> evar_map * constr
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index fbad0d949..214e19fec 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,6 +269,11 @@ let projection_nparams_env env p =
let projection_nparams p = projection_nparams_env (Global.env ()) p
+let has_dependent_elim mib =
+ match mib.mind_record with
+ | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+ | _ -> true
+
(* Annotation for cases *)
let make_case_info env ind style =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -338,6 +343,35 @@ let get_projections env (ind,params) =
| Some (Some (id, projs, pbs)) -> Some projs
| _ -> None
+let make_case_or_project env indf ci pred c branches =
+ let projs = get_projections env indf in
+ match projs with
+ | None -> (mkCase (ci, pred, c, branches))
+ | Some ps ->
+ assert(Array.length branches == 1);
+ let () =
+ let _, _, t = destLambda pred in
+ let (ind, _), _ = dest_ind_family indf in
+ let mib, _ = Inductive.lookup_mind_specif env ind in
+ if (* dependent *) not (noccurn 1 t) &&
+ not (has_dependent_elim mib) then
+ errorlabstrm "make_case_or_project"
+ Pp.(str"Dependent case analysis not allowed" ++
+ str" on inductive type " ++ Names.MutInd.print (fst ind))
+ in
+ let branch = branches.(0) in
+ let ctx, br = decompose_lam_n_assum (Array.length ps) branch in
+ let n, subst =
+ List.fold_right
+ (fun decl (i, subst) ->
+ match decl with
+ | LocalAssum (na, t) ->
+ let t = mkProj (Projection.make ps.(i) true, c) in
+ (i + 1, t :: subst)
+ | LocalDef (na, b, t) -> (i, substl subst b :: subst))
+ ctx (0, [])
+ in substl subst br
+
(* substitution in a signature *)
let substnl_rel_context subst n sign =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index d25f8a837..7bd616591 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -122,11 +122,16 @@ val inductive_has_local_defs : inductive -> bool
val allowed_sorts : env -> inductive -> sorts_family list
+(** (Co)Inductive records with primitive projections do not have eta-conversion,
+ hence no dependent elimination. *)
+val has_dependent_elim : mutual_inductive_body -> bool
+
(** Primitive projections *)
val projection_nparams : projection -> int
val projection_nparams_env : env -> projection -> int
val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
- constr -> types -> types
+ constr -> types -> types
+
(** Extract information from an inductive family *)
@@ -175,6 +180,14 @@ val type_case_branches_with_names :
(** Annotation for cases *)
val make_case_info : env -> inductive -> case_style -> case_info
+(** Make a case or substitute projections if the inductive type is a record
+ with primitive projections.
+ Fail with an error if the elimination is dependent while the
+ inductive type does not allow dependent elimination. *)
+val make_case_or_project :
+ env -> inductive_family -> case_info ->
+ (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr
+
(*i Compatibility
val make_default_case_info : env -> case_style -> inductive -> case_info
i*)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1f6e99c7e..f71719cb9 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -224,12 +224,12 @@ let print_type_in_type ref =
let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
let eta = match recflag with
- | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
- | Decl_kinds.BiFinite -> str " and has eta conversion"
+ | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion"
+ | Decl_kinds.BiFinite -> str " with eta conversion"
in
- [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
+ [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
| _ -> []
-
+
let print_primitive ref =
match ref with
| IndRef ind ->
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index de2818902..99c2d8210 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -95,6 +95,10 @@ let rec_scheme_kind_from_prop =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
(optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
+let rec_scheme_kind_from_type =
+ declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
+ (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
+
let rec_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
(optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index c36797059..77f927f2d 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -13,9 +13,11 @@ open Ind_tables
val rect_scheme_kind_from_prop : individual scheme_kind
val ind_scheme_kind_from_prop : individual scheme_kind
val rec_scheme_kind_from_prop : individual scheme_kind
+val rect_scheme_kind_from_type : individual scheme_kind
val rect_dep_scheme_kind_from_type : individual scheme_kind
val ind_scheme_kind_from_type : individual scheme_kind
val ind_dep_scheme_kind_from_type : individual scheme_kind
+val rec_scheme_kind_from_type : individual scheme_kind
val rec_dep_scheme_kind_from_type : individual scheme_kind
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f18de92c0..4aa7ffa7b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -860,7 +860,7 @@ let descend_then env sigma head dirn =
List.map build_branch
(List.interval 1 (Array.length mip.mind_consnames)) in
let ci = make_case_info env ind RegularStyle in
- mkCase (ci, p, head, Array.of_list brl)))
+ Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl)))
(* Now we need to construct the discriminator, given a discriminable
position. This boils down to:
diff --git a/test-suite/bugs/closed/4622.v b/test-suite/bugs/closed/4622.v
new file mode 100644
index 000000000..ffa478cb8
--- /dev/null
+++ b/test-suite/bugs/closed/4622.v
@@ -0,0 +1,24 @@
+Set Primitive Projections.
+
+Record foo : Type := bar { x : unit }.
+
+Goal forall t u, bar t = bar u -> t = u.
+Proof.
+ intros.
+ injection H.
+ trivial.
+Qed.
+(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *)
+
+(** Dependent pattern-matching is ok on this one as it has eta *)
+Definition baz (x : foo) :=
+ match x as x' return x' = x' with
+ | bar u => eq_refl
+ end.
+
+Inductive foo' : Type := bar' {x' : unit; y: foo'}.
+(** Dependent pattern-matching is not ok on this one *)
+Fail Definition baz' (x : foo') :=
+ match x as x' return x' = x' with
+ | bar' u y => eq_refl
+ end.
diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v
new file mode 100644
index 000000000..f2f917b4e
--- /dev/null
+++ b/test-suite/bugs/closed/4873.v
@@ -0,0 +1,72 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Relation_Definitions.
+Require Import Coq.Compat.Coq85.
+
+Fixpoint tuple' T n : Type :=
+ match n with
+ | O => T
+ | S n' => (tuple' T n' * T)%type
+ end.
+
+Definition tuple T n : Type :=
+ match n with
+ | O => unit
+ | S n' => tuple' T n'
+ end.
+
+Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
+ match n with
+ | 0 => fun x => (x::nil)%list
+ | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list
+ end.
+
+Definition to_list {T} (n:nat) : tuple T n -> list T :=
+ match n with
+ | 0 => fun _ => nil
+ | S n' => fun xs : tuple T (S n') => to_list' n' xs
+ end.
+
+Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n :=
+ match n return _ with
+ | 0 =>
+ match xs return (length xs = 0 -> tuple' T 0) with
+ | nil => fun _ => y
+ | _ => _ (* impossible *)
+ end
+ | S n' =>
+ match xs return (length xs = S n' -> tuple' T (S n')) with
+ | cons x xs' => fun _ => (from_list' x n' xs' _, y)
+ | _ => _ (* impossible *)
+ end
+ end.
+Goal True.
+ pose from_list'_obligation_3 as e.
+ repeat (let e' := fresh in
+ rename e into e';
+ (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e);
+ subst e').
+ progress hnf in e.
+ pose (eq_refl : e = eq_refl).
+ exact I.
+Qed.
+
+Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n :=
+match n return _ with
+| 0 =>
+ match xs return (length xs = 0 -> tuple T 0) with
+ | nil => fun _ : 0 = 0 => tt
+ | _ => _ (* impossible *)
+ end
+| S n' =>
+ match xs return (length xs = S n' -> tuple T (S n')) with
+ | cons x xs' => fun _ => from_list' x n' xs' _
+ | _ => _ (* impossible *)
+ end
+end.
+
+Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs.
+Proof.
+ destruct xs; simpl; intros; subst; auto.
+ generalize dependent t. simpl in *.
+ induction xs; simpl in *; intros; congruence.
+Qed. \ No newline at end of file
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index b5e6ccd61..2fa770494 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -47,7 +47,9 @@ Check _.(next) : option Y.
Lemma eta_ind (y : Y) : y = Build_Y y.(next).
Proof. Fail reflexivity. Abort.
+Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }.
+Fail Scheme Fdef_rec := Induction for Fdef Sort Prop.
(*
Rules for parsing and printing of primitive projections and their eta expansions.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 1e30ab919..54621cc1c 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -8,6 +8,10 @@
(** Compatibility file for making Coq act similar to Coq v8.5 *)
+(** Any compatibility changes to make future versions of Coq behave like Coq 8.6
+ are likely needed to make them behave like Coq 8.5. *)
+Require Export Coq.Compat.Coq86.
+
(* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not
behave as "intros [H|H]" but leave instead hypotheses quantified in
the goal, here producing subgoals A->C and B->C. *)
diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v
new file mode 100644
index 000000000..6952fdf19
--- /dev/null
+++ b/theories/Compat/Coq86.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.6 *) \ No newline at end of file
diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget
index 43b197004..7ffb86ebb 100644
--- a/theories/Compat/vo.itarget
+++ b/theories/Compat/vo.itarget
@@ -1,3 +1,4 @@
AdmitAxiom.vo
Coq84.vo
Coq85.vo
+Coq86.vo
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5438b163a..d9cd574a0 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -130,7 +130,8 @@ let init_ocaml_path () =
[ "grammar" ]; [ "ide" ]; [ "ltac" ]; ]
let get_compat_version = function
- | "8.5" -> Flags.Current
+ | "8.6" -> Flags.Current
+ | "8.5" -> Flags.V8_5
| "8.4" -> Flags.V8_4
| "8.3" -> Flags.V8_3
| "8.2" -> Flags.V8_2
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7c0b9bec2..d141cd8ec 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -200,6 +200,7 @@ let require () =
let add_compat_require v =
match v with
| Flags.V8_4 -> add_require "Coq.Compat.Coq84"
+ | Flags.V8_5 -> add_require "Coq.Compat.Coq85"
| _ -> ()
let compile_list = ref ([] : (bool * string) list)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1e4c3c8f1..b3eae3765 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1147,6 +1147,11 @@ let error_not_allowed_case_analysis isrec kind i =
strbrk " is not allowed for inductive definition " ++
pr_inductive (Global.env()) (fst i) ++ str "."
+let error_not_allowed_dependent_analysis isrec i =
+ str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++
+ strbrk " is not allowed for inductive definition " ++
+ pr_inductive (Global.env()) i ++ str "."
+
let error_not_mutual_in_scheme ind ind' =
if eq_ind ind ind' then
str "The inductive type " ++ pr_inductive (Global.env()) ind ++
@@ -1178,6 +1183,8 @@ let explain_recursion_scheme_error = function
| NotAllowedCaseAnalysis (isrec,k,i) ->
error_not_allowed_case_analysis isrec k i
| NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind'
+ | NotAllowedDependentAnalysis (isrec, i) ->
+ error_not_allowed_dependent_analysis isrec i
(* Pattern-matching errors *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 32e0eb53b..f9e6c207c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -217,7 +217,11 @@ let declare_beq_scheme = declare_beq_scheme_with []
let declare_one_case_analysis_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
- let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
+ let dep =
+ if kind == InProp then case_scheme_kind_from_prop
+ else if not (Inductiveops.has_dependent_elim mib) then
+ case_scheme_kind_from_type
+ else case_dep_scheme_kind_from_type in
let kelim = elim_sorts (mib,mip) in
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
@@ -237,15 +241,23 @@ let kinds_from_type =
InProp,ind_dep_scheme_kind_from_type;
InSet,rec_dep_scheme_kind_from_type]
+let nondep_kinds_from_type =
+ [InType,rect_scheme_kind_from_type;
+ InProp,ind_scheme_kind_from_type;
+ InSet,rec_scheme_kind_from_type]
+
let declare_one_induction_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
let from_prop = kind == InProp in
+ let depelim = Inductiveops.has_dependent_elim mib in
let kelim = elim_sorts (mib,mip) in
let elims =
List.map_filter (fun (sort,kind) ->
if Sorts.List.mem sort kelim then Some kind else None)
- (if from_prop then kinds_from_prop else kinds_from_type) in
+ (if from_prop then kinds_from_prop
+ else if depelim then kinds_from_type
+ else nondep_kinds_from_type) in
List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
elims
@@ -392,7 +404,6 @@ let do_mutual_induction_scheme lnamedepindsort =
let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
let declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 sigma decl in
- (* let decltype = refresh_universes decltype in *)
let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
ConstRef cst :: lrecref
@@ -502,7 +513,8 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
let declare_default_schemes kn =
let mib = Global.lookup_mind kn in
let n = Array.length mib.mind_packets in
- if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then
+ if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+ && mib.mind_typing_flags.check_guarded then
declare_induction_schemes kn;
if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
if is_eq_flag() then try_declare_beq_scheme kn;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 1f1be243e..29d745732 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -858,18 +858,17 @@ let obligation_terminator name num guard hook auto pf =
in
let obl = { obl with obl_status = false, status } in
let uctx = Evd.evar_context_universe_context ctx in
- let (def, obl) = declare_obligation prg obl body ty uctx in
+ let (_, obl) = declare_obligation prg obl body ty uctx in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
try
ignore (update_obls prg obls (pred rem));
- if def then
- if pred rem > 0 then
- begin
- let deps = dependencies obls num in
- if not (Int.Set.is_empty deps) then
+ if pred rem > 0 then
+ begin
+ let deps = dependencies obls num in
+ if not (Int.Set.is_empty deps) then
ignore (auto (Some name) None deps)
- end
+ end
with e when CErrors.noncritical e ->
let e = CErrors.push e in
pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 07:15:58 +0000