diff options
Diffstat (limited to 'pretyping/astterm.ml')
| -rw-r--r-- | pretyping/astterm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/astterm.ml b/pretyping/astterm.ml index 05acff9d7..699a77c49 100644 --- a/pretyping/astterm.ml +++ b/pretyping/astterm.ml @@ -300,6 +300,7 @@ let ref_from_constr = function else RConst (sp,ids_of_ctxt ctxt) | DOPN (MutConstruct (spi,j),ctxt) -> Construct ((spi,j),ids_of_ctxt ctxt) | DOPN (MutInd (sp,i),ctxt) -> Ind (sp,i,ids_of_ctxt ctxt) + | VAR id -> Var id (* utilisé dans trad pour coe_value (tmp) *) | _ -> anomaly "Not a reference" let dbize_ref k sigma env loc s = |