diff options
| author | herbelin | 1999-11-25 01:13:21 +0000 |
|---|---|---|
| committer | herbelin | 1999-11-25 01:13:21 +0000 |
| commit | 2e57237d7518d8cd4ea2b608e5e7c96eb5698638 (patch) | |
| tree | f9319bd7346bb5cde1c6a7d9222337bf909e41da /pretyping/evarutil.ml | |
| parent | e5a040666d1dc58995d7a08e8fe18de90abc7a2d (diff) | |
Des progres dans l'integration
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@140 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |