| Age | Commit message (Collapse) | Author |
|---|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
particulier, TacCall(_,f,[]) est utilisé pour une référence à une
variable ltac ou une tactique et Reference(f) est utilisé pour une
référence à une variable ltac ou un constr (en passant,
standardisation de l'utilisation de constr: ou ltac: à setoid_ring).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10878 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- essai de suppression des dependances debiles. (echec)
- Application des patch debian.
Pour ring et field :
- introduciton de la function de sign et de puissance.
- Correction de certains bug.
- supression de ring_replace ....
Pour exact_no_check :
- ajout de la tactic : vm_cast_no_check (t)
qui remplace "exact_no_check (t<: type of Goal)"
(cette version forcais l'evaluation du cast dans le
pretypage).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9381 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9361 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9315 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9210 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
