From 28e5f4def8bebdaf3bd75b6662bbd4fd88594689 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 12 Nov 2013 19:19:13 +0100
Subject: Better hashconsing of levels and universes, working with modules.
 Huge slowdown to be tracked in some files, even if no polymorphism is
 involved.

Conflicts:
	kernel/univ.ml
---
 tactics/tactics.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 280950600c..75504ee072 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3710,6 +3710,7 @@ let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
    the current goal, abstracted with respect to the local signature,
    is solved by tac *)
 
+(** d1 is the section variable in the global context, d2 in the goal context *)
 let interpretable_as_section_decl d1 d2 = match d2,d1 with
   | (_,Some _,_), (_,None,_) -> false
   | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 && eq_constr t1 t2
-- 
cgit v1.2.3