aboutsummaryrefslogtreecommitdiff
path: root/tactics/eauto.ml
AgeCommit message (Expand)Author
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
2016-10-26Using msg_info for info_auto and info_eauto (PR #324).Hugo Herbelin
2016-10-25Remove v62 from the codebase.Théo Zimmermann
2016-10-21sections/hints: prevent Not_found in get_type_ofMatthieu Sozeau
2016-10-14Fixing English typography for colon.Hugo Herbelin
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-04Do not normalize evars in Eauto.e_give_exact.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-16Put the "exact" family of tactic in the monad.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
2016-03-06Removing useless grammar.cma dependencies.Pierre-Marie Pédrot
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
2001-11-05GROS COMMIT:barras
2001-06-29Autoriser Apply avec un but sous forme d'implication ou de quantificationbarras
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-03-08changement comparaison etatsfilliatr
2001-03-06Modification de e_give_exact pour eviter d'echouer sur l'unificationmohring
2001-03-06eta-expansionmohring
2001-03-06EAutod (debug)filliatr
2001-03-05module Explore générique et réécriture EAuto avec ce module; occur check ...filliatr
2001-02-28modifmohring
2001-02-27EAuto mixte (largeur puis profondeur)mohring
2001-02-26Eauto version en largeurmohring
2000-11-23Reparation IsMutConstruct + Transparentmohring
2000-11-02suppression des (* open Generic *)filliatr
2000-10-13Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...herbelin
2000-10-11Prise en compte de l'env local dans make_apply_entryherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-06-28Modifs de presentation.delahaye
2000-06-21portage EAuto et Ringfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 16:03:51 +0000