diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /pretyping/patternops.ml | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index fd76a9473f..ee79b54744 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -12,6 +12,7 @@ open Names open Globnames open Nameops open Term +open Constr open Vars open Glob_term open Pp @@ -75,8 +76,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) = and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && - Array.equal Term.eq_constr c1 c2 && - Array.equal Term.eq_constr r1 r2 + Array.equal Constr.equal c1 c2 && + Array.equal Constr.equal r1 r2 let rec occur_meta_pattern = function | PApp (f,args) -> @@ -149,7 +150,7 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with let pattern_of_constr env sigma t = let rec pattern_of_constr env t = let open Context.Rel.Declaration in - match kind_of_term t with + match kind t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id @@ -165,7 +166,7 @@ let pattern_of_constr env sigma t = pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match - match kind_of_term f with + match kind f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id |