aboutsummaryrefslogtreecommitdiff
path: root/kernel/pre_env.ml
AgeCommit message (Collapse)Author
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-27Modification de la vm:notin
- le type val_kind n'embarque plus le constr (pb de cohérence avec le context); - en revanche, lors du calcul d'une valeur, on calcule aussi l'ensemble des variables nommées dont la valeur peut dépendre; - lors du clear_hyps, si la valeur dépend d'une variable effacée, on invalide le calcul. Corrige le bug #1419 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9733 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-12correction bugs de condition de garde (fix + cofix)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8810 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-06j'avais oublie ces deux fichiers.gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7642 85f007b7-540e-0410-9357-904b9bb8a0f7