diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
| commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
| tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /pretyping/cbv.mli | |
| parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) | |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'pretyping/cbv.mli')
| -rw-r--r-- | pretyping/cbv.mli | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 87a03abb..cdaa39c5 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,13 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term +open EConstr open Environ open CClosure open Esubst @@ -23,6 +25,9 @@ val cbv_norm : cbv_infos -> constr -> constr (*********************************************************************** i This is for cbv debug *) + +open Constr + type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack @@ -30,13 +35,13 @@ type cbv_value = | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array - | CONSTR of constructor puniverses * cbv_value array + | CONSTR of constructor Univ.puniverses * cbv_value array and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of projection * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack val shift_value : int -> cbv_value -> cbv_value |