diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-11-12 19:19:13 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:55 +0200 |
| commit | 28e5f4def8bebdaf3bd75b6662bbd4fd88594689 (patch) | |
| tree | 3f4dd3966b7be0ade898b6fceb055918e76f8ae1 /tactics/tactics.ml | |
| parent | de1f3069045e5b21804b9f58a3510999ef580c84 (diff) | |
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
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 280950600..75504ee07 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 |