aboutsummaryrefslogtreecommitdiff
path: root/contrib/first-order
AgeCommit message (Collapse)Author
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13factorisation et generalisation des clausesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ground update changing left-arrow-arrow rule.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4623 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom ↵herbelin
indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Passage à la V8 par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-11Ground bugfixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4235 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-08Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4227 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-04Ground bugfixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4220 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-03switching back to old tautocorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4219 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-03modification groundcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4218 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-03addition of Auto hints in Groundcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4217 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-02added hints into Groundcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4215 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-22Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4196 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4193 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20Ground Update.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4171 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-16ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4169 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-15Ground major update ... mmm, sounds exciting !corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4167 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4166 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Major Ground update, may break semanticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4164 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4158 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground update, new files.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4156 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Ground update.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4144 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur ↵herbelin
de tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4125 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-04bugfix for Ground ( merci JC )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4097 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-04Ground update + some bugfixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4096 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Ground daily updatecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4090 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26GIntuition now matches Intuition up to hyps renaming.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4080 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26Added breakpoint in Ground tactic.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4079 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-26moved engine.ml4 to ground.ml4, added option 'Ground Depth'corbinea
fixed utf8.vo dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4078 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-25Ground and CCsolve updatescorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-16Major Ground tactic update, sensible performance improvementcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4026 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-08bugfixes in Ground.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3997 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07Enhancement of the Ground tactic, addition of GTauto and GIntuition.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-26bugfix in Ground tacticcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3957 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-25Added the Ground tactic.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7