diff options
| author | Hugo Herbelin | 2016-12-22 13:48:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-12-22 13:48:01 +0100 |
| commit | ac630f12c9d80c9387d44f3f1a1b22db5b5b89da (patch) | |
| tree | fb06dddfc8eb348b93fb4cb34d4fcf4ed08933e7 | |
| parent | 9c0bec7cb273ec00be45bfe728f87150c3d2f925 (diff) | |
Fixing anomaly EqUnknown in Equality Scheme (#5278).
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 18 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 3 |
2 files changed, 12 insertions, 9 deletions
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) |