diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 21 |
1 files changed, 3 insertions, 18 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 64a2dd9d1a..99de984322 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1,30 +1,15 @@ -(****************************************************************************) -(* The Calculus of Inductive Constructions *) -(* *) -(* Projet Coq *) -(* *) -(* INRIA LRI-CNRS ENS-CNRS *) -(* Rocquencourt Orsay Lyon *) -(* *) -(* Coq V6.3 *) -(* July 1st 1999 *) -(* *) -(****************************************************************************) -(* tradevar.ml *) -(****************************************************************************) - -open Std;; +(* $Id$ *) + +open Util;; open Pp;; open Names;; open Impuniv;; -open Vectops;; open Generic;; open Term;; open Printer;; open Termenv;; open Evd;; open Reduction;; -open Himsg;; let rec filter_unique = function |