diff options
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 |
