diff options
| author | Pierre-Marie Pédrot | 2016-10-02 02:01:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-02 02:07:27 +0200 |
| commit | 527d3525b726f8136b64c7c1cf770c702f966cad (patch) | |
| tree | cc7afb6284d3cf6bf571fa330516884529f0aadb | |
| parent | 109e05059692d0f2f15a4b1699ff4a25d07e5a79 (diff) | |
Fix bug #5069: Scheme Equality gives anomalies in sections.
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 12 | ||||
| -rw-r--r-- | toplevel/auto_ind_decl.mli | 2 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 |
3 files changed, 11 insertions, 5 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 180b836ea5..0561fc4b82 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -54,7 +54,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of constant +exception ParameterWithoutEquality of global_reference exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported @@ -181,7 +181,13 @@ let build_beq_scheme mode kn = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants + | Var x -> + let eid = id_of_string ("eq_"^(string_of_id x)) in + let () = + try ignore (Environ.lookup_named eid env) + with Not_found -> raise (ParameterWithoutEquality (VarRef x)) + in + mkVar eid, Safe_typing.empty_private_constants | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> @@ -209,7 +215,7 @@ let build_beq_scheme mode kn = | LetIn _ -> raise (EqUnknown "LetIn") | Const kn -> (match Environ.constant_opt_value_in env kn with - | None -> raise (ParameterWithoutEquality (fst kn)) + | None -> raise (ParameterWithoutEquality (ConstRef (fst kn))) | Some c -> aux (applist (c,a))) | Proj _ -> raise (EqUnknown "Proj") | Construct _ -> raise (EqUnknown "Construct") diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index b6c66a1e84..fa5c61484e 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -21,7 +21,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of constant +exception ParameterWithoutEquality of Globnames.global_reference exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index f9e6c207c3..e8ea617f45 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -161,7 +161,7 @@ let try_declare_scheme what f internal names kn = let msg = match fst e with | ParameterWithoutEquality cst -> alarm what internal - (str "Boolean equality not found for parameter " ++ pr_con cst ++ + (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++ str".") | InductiveWithProduct -> alarm what internal |