diff options
| author | Maxime Dénès | 2020-07-03 10:11:22 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-03 10:11:22 +0200 |
| commit | 33581635d3ad525e1d5c2fb2587be345a7e77009 (patch) | |
| tree | 1aff9ab6c08d8aa1cee6987875ffbe010ebbc74a /pretyping/unification.ml | |
| parent | ce500b3483bbc80ee8baee3b255c3b09b5b2b17e (diff) | |
| parent | 0c6c495b92186ee357eb6b6a5ff62826040f549c (diff) | |
Merge PR #10390: UIP in SProp
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 95b07e227e..ef58f41489 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -567,7 +567,7 @@ let is_rigid_head sigma flags t = | Construct _ | Int _ | Float _ -> true | Fix _ | CoFix _ -> true | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _ - | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _) + | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _) | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = @@ -657,7 +657,7 @@ let rec is_neutral env sigma ts t = not (TransparentState.is_transparent_variable ts id) | Rel n -> true | Evar _ | Meta _ -> true - | Case (_, p, c, cl) -> is_neutral env sigma ts c + | Case (_, p, _, c, _) -> is_neutral env sigma ts c | Proj (p, c) -> is_neutral env sigma ts c | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ -> false | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *) @@ -847,7 +847,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> raise ex) - | Case (ci1,p1,c1,cl1), Case (ci2,p2,c2,cl2) -> + | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) -> (try if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN); let opt' = {opt with at_top = true; with_types = false} in @@ -1782,7 +1782,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = matchrec c1 with ex when precatchable_exception ex -> matchrec c2) - | Case(_,_,c,lf) -> (* does not search in the predicate *) + | Case(_,_,_,c,lf) -> (* does not search in the predicate *) (try matchrec c with ex when precatchable_exception ex -> @@ -1867,7 +1867,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = let c2 = args.(n-1) in bind (matchrec c1) (matchrec c2) - | Case(_,_,c,lf) -> (* does not search in the predicate *) + | Case(_,_,_,c,lf) -> (* does not search in the predicate *) bind (matchrec c) (bind_iter matchrec lf) | Proj (p,c) -> matchrec c |