diff options
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index bf28e0850..880f8a4be 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -18,19 +18,17 @@ open Topconstr open Termops open Pretyping -(** {6 Sect } *) -(** Translation from front abstract syntax of term to untyped terms (rawconstr) +(** Translation from front abstract syntax of term to untyped terms (rawconstr) *) - The translation performs: +(** The translation performs: - resolution of names : - check all variables are bound - make absolute the references to global objets - resolution of symbolic notations using scopes - insert existential variables for implicit arguments -*) -(** To interpret implicits and arg scopes of recursive variables while + To interpret implicits and arg scopes of recursive variables while internalizing inductive types and recursive definitions, and also projection while typing records. |