versions of glob that ignore universes.

gmalecha · Jun 5, 2015 · 1ecde10 · 1ecde10
1 parent 577afe6
commit 1ecde10
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git a/src/term_match.ml b/src/term_match.ml
@@ -1,6 +1,8 @@
 type ('a,'b,'c) pattern =
 | Glob of Term.constr Lazy.t
 | EGlob of Term.constr
+| Glob_no_univ of Term.constr Lazy.t
+| EGlob_no_univ of Term.constr
 | App of ('a,'b,'c) pattern * ('a,'b,'c) pattern
 | Lam of 'b * ('a,'b,'c) pattern * ('a,'b,'c) pattern
 | As of ('a,'b,'c) pattern * 'a
@@ -43,6 +45,22 @@ let rec match_pattern p e ctx s =
       else
 	raise Match_failure
     end
+  | Glob_no_univ name ->
+    begin
+      if Term.eq_constr_nounivs (Lazy.force name) e
+      then
+	s
+      else
+	raise Match_failure
+    end
+  | EGlob_no_univ name ->
+    begin
+      if Term.eq_constr_nounivs name e
+      then
+	s
+      else
+	raise Match_failure
+    end
   | Filter (f, p) ->
     if f ctx e then match_pattern p e ctx s else raise Match_failure
   | Choice pl ->

diff --git a/src/term_match.mli b/src/term_match.mli
@@ -1,6 +1,8 @@
 type ('a,'b,'c) pattern =
 | Glob of Term.constr Lazy.t
 | EGlob of Term.constr
+| Glob_no_univ of Term.constr Lazy.t
+| EGlob_no_univ of Term.constr
 | App of ('a,'b,'c) pattern * ('a,'b,'c) pattern
 | Lam of 'b * ('a,'b,'c) pattern * ('a,'b,'c) pattern
 | As of ('a,'b,'c) pattern * 'a