diff options
| author | filliatr | 2000-11-02 14:33:31 +0000 |
|---|---|---|
| committer | filliatr | 2000-11-02 14:33:31 +0000 |
| commit | e59113f1bdf4d8c98d956c01f51ae019942d92cd (patch) | |
| tree | c1ef110c92fbab4112b3e8584e8a8b649f435a70 /pretyping | |
| parent | f0a793f123683eaab6bab9968725febe7c311f05 (diff) | |
suppression des (* open Generic *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 1 | ||||
| -rw-r--r-- | pretyping/class.ml | 1 | ||||
| -rwxr-xr-x | pretyping/classops.ml | 1 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 1 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 1 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 1 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 1 | ||||
| -rwxr-xr-x | pretyping/recordops.ml | 5 | ||||
| -rwxr-xr-x | pretyping/recordops.mli | 1 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 1 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 1 | ||||
| -rw-r--r-- | pretyping/typing.ml | 1 |
13 files changed, 0 insertions, 17 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 413ea152a2..84041fb329 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,7 +1,6 @@ open Util open Names -(* open Generic *) open Term open Declarations open Inductive diff --git a/pretyping/class.ml b/pretyping/class.ml index 0f201d004f..0ea8e3113a 100644 --- a/pretyping/class.ml +++ b/pretyping/class.ml @@ -4,7 +4,6 @@ open Util open Pp open Names -(* open Generic *) open Term open Inductive open Declarations diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 36b5ed4d53..249633cbdf 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -9,7 +9,6 @@ open Environ open Libobject open Declare open Term -(* open Generic *) open Rawterm (* usage qque peu general: utilise aussi dans record *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6280fc392b..ad518380dc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,7 +1,6 @@ (* $Id$ *) open Util -(* open Generic *) open Names open Term open Reduction diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 70eba2949e..3ed28a91e4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -5,7 +5,6 @@ open Pp open Util open Univ open Names -(* open Generic *) open Term open Inductive open Sign diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index fd52e0fa0f..3316e23816 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -3,7 +3,6 @@ open Util open Names -(* open Generic *) open Term open Reduction open Instantiate diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index ce08a0f390..72e46b52b0 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -5,7 +5,6 @@ open Util open Pp open Names open Univ -(* open Generic *) open Term open Sign open Environ diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 67e793c54f..5101173308 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -4,7 +4,6 @@ open Pp open Util open Names -(* open Generic *) open Sign open Evd open Term diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f16f77c631..9efd881fac 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -9,11 +9,6 @@ open Typeops open Libobject open Library open Classops -(* -open Pp_control -(* open Generic *) -open Initial -*) let nbimpl = ref 0 let nbpathc = ref 0 diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 97c6c53069..8ad0203b35 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -4,7 +4,6 @@ (*i*) open Names open Term -(* open Generic *) open Classops open Libobject open Library diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 53bf5b08a7..22eba722cc 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -5,7 +5,6 @@ open Util open Term open Inductive open Names -(* open Generic *) open Reduction open Environ open Typeops diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 77f8cf9e11..653a08fdc0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -4,7 +4,6 @@ open Pp open Util open Names -(* open Generic *) open Term open Inductive open Environ diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 23028cc626..3f0ab9501a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -3,7 +3,6 @@ open Util open Names -(* open Generic *) open Term open Environ open Reduction |
