diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 0818a55256..c36542aebc 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -112,14 +112,14 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") + | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> ConstRef sp | Construct (sp,_) -> ConstructRef sp | Ind (sp,_) -> IndRef sp | Var id -> VarRef id - | _ -> anomaly (Pp.str "Not a rigid reference") + | _ -> anomaly (Pp.str "Not a rigid reference.") let pattern_of_constr env sigma t = let rec pattern_of_constr env t = @@ -143,7 +143,7 @@ let pattern_of_constr env sigma t = match kind_of_term f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> Some id + Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id | _ -> None) | _ -> None with @@ -156,13 +156,14 @@ let pattern_of_constr env sigma t = pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - assert (not b); PMeta (Some id) + | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) -> + PMeta (Some id) | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) else PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) | Case (ci,p,a,br) -> @@ -329,12 +330,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) - | GPatVar (false,n) -> + | GPatVar (Evar_kinds.FirstOrderPatVar n) -> metas := n::!metas; PMeta (Some n) | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ({ CAst.v = GPatVar (true,n) }, cl) -> + | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (c,cl) -> PApp (pat_of_raw metas vars c, @@ -363,9 +364,9 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda c na = CAst.make ?loc @@ + let mkGLambda na c = CAst.make ?loc @@ GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in - let c = List.fold_left mkGLambda c nal in + let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; |