aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml51
1 files changed, 24 insertions, 27 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a9..c3f392980 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -32,7 +32,6 @@ open Evardefine
open Evarsolve
open Evarconv
open Evd
-open Sigma.Notations
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -70,7 +69,7 @@ let error_wrong_numarg_inductive ?loc env c n =
let list_try_compile f l =
let rec aux errors = function
- | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors)
+ | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors)
| h::t ->
try f h
with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
@@ -162,9 +161,9 @@ let feed_history arg = function
| Continuation (n, l, h) when n>=1 ->
Continuation (n-1, arg :: l, h)
| Continuation (n, _, _) ->
- anomaly (str "Bad number of expected remaining patterns: " ++ int n)
+ anomaly (str "Bad number of expected remaining patterns: " ++ int n ++ str ".")
| Result _ ->
- anomaly (Pp.str "Exhausted pattern history")
+ anomaly (Pp.str "Exhausted pattern history.")
(* This is for non exhaustive error message *)
@@ -190,7 +189,7 @@ let pop_history_pattern = function
| Continuation (0, l, MakeConstructor (pci, rh)) ->
feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh
| _ ->
- anomaly (Pp.str "Constructor not yet filled with its arguments")
+ anomaly (Pp.str "Constructor not yet filled with its arguments.")
let pop_history h =
feed_history (CAst.make @@ PatVar Anonymous) h
@@ -425,7 +424,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
let current_pattern eqn =
match eqn.patterns with
| pat::_ -> pat
- | [] -> anomaly (Pp.str "Empty list of patterns")
+ | [] -> anomaly (Pp.str "Empty list of patterns.")
let alias_of_pat = CAst.with_val (function
| PatVar name -> name
@@ -438,7 +437,7 @@ let remove_current_pattern eqn =
{ eqn with
patterns = pats;
alias_stack = alias_of_pat pat :: eqn.alias_stack }
- | [] -> anomaly (Pp.str "Empty list of patterns")
+ | [] -> anomaly (Pp.str "Empty list of patterns.")
let push_current_pattern (cur,ty) eqn =
match eqn.patterns with
@@ -447,7 +446,7 @@ let push_current_pattern (cur,ty) eqn =
{ eqn with
rhs = { eqn.rhs with rhs_env = rhs_env };
patterns = pats }
- | [] -> anomaly (Pp.str "Empty list of patterns")
+ | [] -> anomaly (Pp.str "Empty list of patterns.")
(* spiwack: like [push_current_pattern] but does not introduce an
alias in rhs_env. Aliasing binders are only useful for variables at
@@ -457,7 +456,7 @@ let push_noalias_current_pattern eqn =
match eqn.patterns with
| _::pats ->
{ eqn with patterns = pats }
- | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns")
+ | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns.")
@@ -641,7 +640,7 @@ let replace_tomatch sigma n c =
| Pushed (initial,((b,tm),l,na)) :: rest ->
let b = replace_term sigma n c depth b in
let tm = map_tomatch_type (replace_term sigma n c depth) tm in
- List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l;
+ List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch.")) l;
Pushed (initial,((b,tm),l,na)) :: replrec depth rest
| Alias (initial,(na,b,d)) :: rest ->
(* [b] is out of replacement scope *)
@@ -731,7 +730,7 @@ let get_names env sigma sign eqns =
(fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
d na
in
- (na::l,(out_name na)::avoid))
+ (na::l,(Name.get_id na)::avoid))
([],allvars) (List.rev sign) names2 in
names3,aliasname
@@ -882,7 +881,7 @@ let specialize_predicate_var (cur,typ,dep) env tms ccl =
(*****************************************************************************)
let generalize_predicate sigma (names,na) ny d tms ccl =
let () = match na with
- | Anonymous -> anomaly (Pp.str "Undetected dependency")
+ | Anonymous -> anomaly (Pp.str "Undetected dependency.")
| _ -> () in
let p = List.length names + 1 in
let ccl = lift_predicate 1 ccl tms in
@@ -1708,7 +1707,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
evdref := evd;
(t,tt) in
let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
- if not b then anomaly (Pp.str "Build_tycon: should be a type");
+ if not b then anomaly (Pp.str "Build_tycon: should be a type.");
{ uj_val = t; uj_type = tt }
(* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1872,7 +1871,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
if not (eq_ind ind ind') then
user_err ?loc (str "Wrong inductive type.");
if not (Int.equal nrealargs_ctxt (List.length realnal)) then
- anomaly (Pp.str "Ill-formed 'in' clause in cases");
+ anomaly (Pp.str "Ill-formed 'in' clause in cases.");
List.rev realnal
| None -> List.make nrealargs_ctxt Anonymous in
LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf'))
@@ -2000,10 +1999,8 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
let sigma,t = match tycon with
| Some t -> refresh_tycon sigma t
| None ->
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma ((t, _), sigma, _) =
+ let (sigma, (t, _)) =
new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
- let sigma = Sigma.to_evar_map sigma in
sigma, t
in
(* First strategy: we build an "inversion" predicate *)
@@ -2064,8 +2061,8 @@ let mk_JMeq evdref typ x typ' y =
let mk_JMeq_refl evdref typ x =
papp evdref coq_JMeq_refl [| typ; x |]
-let hole = CAst.make @@
- GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole na = CAst.make @@
+ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
Misctypes.IntroAnonymous, None)
let constr_of_pat env evdref arsign pat avoid =
@@ -2168,7 +2165,7 @@ let vars_of_ctx sigma ctx =
prev,
(CAst.make @@ GApp (
(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)),
- [hole; CAst.make @@ GVar prev])) :: vars
+ [hole na; CAst.make @@ GVar prev])) :: vars
| _ ->
match RelDecl.get_name decl with
Anonymous -> invalid_arg "vars_of_ctx"
@@ -2223,14 +2220,14 @@ let build_ineqs evdref prevpatterns pats liftsign =
(Some ([], 0, 0, [])) eqnpats pats
in match acc with
None -> c
- | Some (sign, len, _, c') ->
- let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c'))
- (lift_rel_context liftsign sign)
- in
- conj :: c)
+ | Some (sign, len, _, c') ->
+ let sigma, conj = mk_coq_and !evdref c' in
+ let sigma, neg = mk_coq_not sigma conj in
+ let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in
+ evdref := sigma; conj :: c)
[] prevpatterns
in match diffs with [] -> None
- | _ -> Some (mk_coq_and diffs)
+ | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj)
let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
let i = ref 0 in
@@ -2301,7 +2298,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
| l -> CAst.make @@ GApp (bref, l)
in
let branch = match ineqs with
- Some _ -> CAst.make @@ GApp (branch, [ hole ])
+ Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
| None -> branch
in
incr i;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 18:30:22 +0000