diff options
Diffstat (limited to 'pretyping/rawterm.ml')
| -rw-r--r-- | pretyping/rawterm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 62798a45..3726b8df 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: rawterm.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: rawterm.ml 11282 2008-07-28 11:51:53Z msozeau $ *) (*i*) open Util @@ -36,7 +36,7 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option type binder_kind = BProd | BLambda | BLetIn -type binding_kind = Explicit | Implicit +type binding_kind = Lib.binding_kind = Explicit | Implicit type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier |