From 5fa47f1258408541150e2e4c26d60ff694e7c1bc Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:37 +0000 Subject: locus.mli for occurrences+clauses, misctypes.mli for various little things Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pattern.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'pretyping/pattern.ml') diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 47cc57fd1..ef81aa4d3 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -17,6 +17,8 @@ open Environ open Nametab open Pp open Mod_subst +open Misctypes +open Decl_kinds (* Metavariables *) @@ -100,7 +102,8 @@ let pattern_of_constr sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort (Prop c) -> PSort (GProp c) + | Sort (Prop Null) -> PSort GProp + | Sort (Prop Pos) -> PSort GSet | Sort (Type _) -> PSort (GType None) | Cast (c,_,_) -> pattern_of_constr c | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) -- cgit v1.2.3