diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-24 13:39:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-24 13:39:23 +0000 |
| commit | 3afaf3dde673d77cacaabc354f008dfbe49a7cee (patch) | |
| tree | 4264164faf763ab8d18274cd5aeffe5a1de21728 /parsing/termast.mli | |
| parent | 83f038e61a4424fcf71aada9f97c91165b73aef8 (diff) | |
Passage à des contextes de vars et de rels pouvant contenir des déclarations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.mli')
| -rw-r--r-- | parsing/termast.mli | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/parsing/termast.mli b/parsing/termast.mli index 7961ee7fb..4e62177a9 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -5,6 +5,7 @@ open Names open Term open Sign +open Environ open Rawterm open Pattern (*i*) @@ -14,21 +15,21 @@ open Pattern val ast_of_cases_pattern : cases_pattern -> Coqast.t val ast_of_rawconstr : rawconstr -> Coqast.t -val ast_of_pattern : unit assumptions -> constr_pattern -> Coqast.t +val ast_of_pattern : names_context -> constr_pattern -> Coqast.t (* If [b=true] in [ast_of_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed *) -val ast_of_constr : bool -> unit assumptions -> constr -> Coqast.t +val ast_of_constr : bool -> env -> constr -> Coqast.t (*i C'est bdize qui sait maintenant s'il faut afficher les casts ou pas val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t i*) -val ast_of_constant : unit assumptions -> constant -> Coqast.t -val ast_of_existential : unit assumptions -> existential -> Coqast.t -val ast_of_constructor : unit assumptions -> constructor -> Coqast.t -val ast_of_inductive : unit assumptions -> inductive -> Coqast.t +val ast_of_constant : env -> constant -> Coqast.t +val ast_of_existential : env -> existential -> Coqast.t +val ast_of_constructor : env -> constructor -> Coqast.t +val ast_of_inductive : env -> inductive -> Coqast.t (* For debugging *) val print_implicits : bool ref |