Skip to content
Browse files

- Relax identification of metas in Ltac to not compare universes synt…

…actically.

- add constr_eq_nounivs tactic to compare constrs without comparing universes.
  • Loading branch information...
1 parent e13239c commit e88e47ca76200a5e52bd0f9397fe4900fa9b241b @mattam82 mattam82 committed Aug 1, 2013
Showing with 6 additions and 1 deletion.
  1. +1 −1 pretyping/matching.ml
  2. +5 −0 tactics/extratactics.ml4
View
2 pretyping/matching.ml
@@ -50,7 +50,7 @@ exception PatternMatchingFailure
let constrain n (ids, m as x) (names, terms as subst) =
try
let (ids',m') = List.assoc n terms in
- if List.equal Id.equal ids ids' && eq_constr m m' then subst
+ if List.equal Id.equal ids ids' && eq_constr_nounivs m m' then subst
else raise PatternMatchingFailure
with
Not_found ->
View
5 tactics/extratactics.ml4
@@ -741,6 +741,11 @@ TACTIC EXTEND constr_eq
if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ]
END
+TACTIC EXTEND constr_eq_nounivs
+| [ "constr_eq_nounivs" constr(x) constr(y) ] -> [
+ if eq_constr_nounivs x y then tclIDTAC else tclFAIL 0 (str "Not equal") ]
+END
+
TACTIC EXTEND is_evar
| [ "is_evar" constr(x) ] ->
[ match kind_of_term x with

0 comments on commit e88e47c

Please sign in to comment.
Something went wrong with that request. Please try again.