diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-19 10:03:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-19 10:03:07 +0000 |
| commit | 6f600fd1c528c97f7d2e1016af1650ab62b2b4c1 (patch) | |
| tree | e4d31f993f8ca7452839c8d944ad737662394d6b | |
| parent | 5865d4d79f052cfb190e728e8618cb05e2ac845f (diff) | |
Version préliminaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@124 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 = |