diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-21 00:17:21 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:01:21 +0100 |
commit | 6899d3aa567436784a08af4e179c2ef1fa504a02 (patch) | |
tree | 41ff9881c85242d2f58eb59364be3d8fa14e851c /proofs/logic.ml | |
parent | e7f7fc3e0582867975642fcaa7bd42140c61cd99 (diff) |
Moving extended_rel_vect/extended_rel_list to the kernel.
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
Diffstat (limited to 'proofs/logic.ml')
-rw-r--r-- | proofs/logic.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index e80f5a64c..1ba14e7d4 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -13,6 +13,7 @@ open Names open Nameops open Term open Vars +open Context open Termops open Environ open Reductionops |