diff options
Diffstat (limited to 'parsing/astterm.mli')
| -rw-r--r-- | parsing/astterm.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/astterm.mli b/parsing/astterm.mli index be9c7b1a7..31d96145a 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -20,6 +20,10 @@ open Pattern (* Translation from AST to terms. *) +(* To embed constr in Coqast.t *) +val constrIn : constr -> Coqast.t +val constrOut : Coqast.t -> constr + val interp_rawconstr : 'a evar_map -> env -> Coqast.t -> rawconstr val interp_constr : 'a evar_map -> env -> Coqast.t -> constr val interp_casted_constr : 'a evar_map -> env -> Coqast.t -> constr -> constr |