From ac630f12c9d80c9387d44f3f1a1b22db5b5b89da Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Dec 2016 13:48:01 +0100 Subject: Fixing anomaly EqUnknown in Equality Scheme (#5278). --- toplevel/auto_ind_decl.ml | 18 +++++++++--------- toplevel/indschemes.ml | 3 +++ 2 files changed, 12 insertions(+), 9 deletions(-) (limited to 'toplevel') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index b3144fa927..a527be32ba 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -204,19 +204,19 @@ let build_beq_scheme mode kn = end | Sort _ -> raise InductiveWithSort | Prod _ -> raise InductiveWithProduct - | Lambda _-> raise (EqUnknown "Lambda") - | LetIn _ -> raise (EqUnknown "LetIn") + | Lambda _-> raise (EqUnknown "abstraction") + | LetIn _ -> raise (EqUnknown "let-in") | Const kn -> (match Environ.constant_opt_value_in env kn with | None -> raise (ParameterWithoutEquality (fst kn)) | Some c -> aux (applist (c,a))) - | Proj _ -> raise (EqUnknown "Proj") - | Construct _ -> raise (EqUnknown "Construct") - | Case _ -> raise (EqUnknown "Case") - | CoFix _ -> raise (EqUnknown "CoFix") - | Fix _ -> raise (EqUnknown "Fix") - | Meta _ -> raise (EqUnknown "Meta") - | Evar _ -> raise (EqUnknown "Evar") + | Proj _ -> raise (EqUnknown "projection") + | Construct _ -> raise (EqUnknown "constructor") + | Case _ -> raise (EqUnknown "match") + | CoFix _ -> raise (EqUnknown "cofix") + | Fix _ -> raise (EqUnknown "fix") + | Meta _ -> raise (EqUnknown "meta-variable") + | Evar _ -> raise (EqUnknown "existential variable") in aux t in diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index aa2362ae5f..0e59f1aa98 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -185,6 +185,9 @@ let try_declare_scheme what f internal names kn = | DecidabilityMutualNotSupported -> alarm what internal (str "Decidability lemma for mutual inductive types not supported.") + | EqUnknown s -> + alarm what internal + (str "Found unsupported " ++ str s ++ str " while building Boolean equality.") | e when Errors.noncritical e -> alarm what internal (str "Unexpected error during scheme creation: " ++ Errors.print e) -- cgit v1.2.3 From 3b821bf60d89c386c27487e172e57a669b5c4662 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 23 Dec 2016 11:53:17 +0100 Subject: Excluding explicitly coinductive types in Scheme Equality (#5284). --- toplevel/auto_ind_decl.ml | 3 +++ toplevel/auto_ind_decl.mli | 1 + toplevel/indschemes.ml | 3 +++ 3 files changed, 7 insertions(+) (limited to 'toplevel') diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index a527be32ba..ace99b7bbe 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -56,6 +56,7 @@ exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported +exception NoDecidabilityCoInductive let dl = Loc.ghost @@ -301,6 +302,8 @@ let build_beq_scheme mode kn = let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in if not (Sorts.List.mem InSet kelim) then raise (NonSingletonProp (kn,i)); + if mib.mind_finite = Decl_kinds.CoFinite then + raise NoDecidabilityCoInductive; let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), Evd.make_evar_universe_context (Global.env ()) None), diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index b6c66a1e84..bdfe6e3fa7 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -24,6 +24,7 @@ exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported +exception NoDecidabilityCoInductive val beq_scheme_kind : mutual scheme_kind val build_beq_scheme : mutual_scheme_object_function diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 0e59f1aa98..a430d0ded2 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -188,6 +188,9 @@ let try_declare_scheme what f internal names kn = | EqUnknown s -> alarm what internal (str "Found unsupported " ++ str s ++ str " while building Boolean equality.") + | NoDecidabilityCoInductive -> + alarm what internal + (str "Scheme Equality is only for inductive types.") | e when Errors.noncritical e -> alarm what internal (str "Unexpected error during scheme creation: " ++ Errors.print e) -- cgit v1.2.3 From dd710b9adbe7b27dccd6d4b21b90cb9bd07e5c07 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 26 Dec 2016 10:02:34 +0100 Subject: Fix some documentation typos. --- toplevel/vernacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c76432ae3e..1328019713 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2050,7 +2050,7 @@ let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () | Some b -> Flags.make_polymorphic_flag b; b -(** A global default timeout, controled by option "Set Default Timeout n". +(** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) let default_timeout = ref None -- cgit v1.2.3 From 6e4c4578044c15ec172009a570d13b9e168cb93e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 28 Jan 2017 19:02:20 +0100 Subject: Fix bug #5262: Error should tell me which name is duplicated. --- toplevel/record.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'toplevel') diff --git a/toplevel/record.ml b/toplevel/record.ml index ef09f6fa54..b8dcf81fde 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -550,8 +550,10 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc | _ -> acc in let allnames = idstruc::(List.fold_left extract_name [] fs) in - if not (List.distinct_f Id.compare allnames) - then error "Two objects have the same name"; + let () = match List.duplicates Id.equal allnames with + | [] -> () + | id :: _ -> errorlabstrm "" (str "Two objects have the same name" ++ spc () ++ quote (Id.print id)) + in let isnot_class = match kind with Class false -> false | _ -> true in if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then error "Priorities only allowed for type class substructures"; -- cgit v1.2.3