aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-01-30Get rid of two utility files, obsolete now that configure is a .mlPierre Letouzey
2014-01-30clib.mllib: remove duplicated Flags entryPierre Letouzey
2014-01-30G_xml: remove some duplication in error fonctionsPierre Letouzey
2014-01-30G_xml: protect against some possible Not_foundPierre Letouzey
2014-01-30Load implemented in CoqIDE/STM (closes: #3223)Enrico Tassi
2014-01-30STM + CoqIDE: stop_worker message and UIEnrico Tassi
2014-01-30Work around for bug in threads + blocking io streamlinedEnrico Tassi
2014-01-30STM: worker sends back to master the last valid stateEnrico Tassi
So that the master process does not require to compute it. Still not all valid states are sent back.
2014-01-30STM: tell the user if the master is recomputing states validated by workersEnrico Tassi
When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly.
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2014-01-29Using Map.smartmap whenever deemed useful.Pierre-Marie Pédrot
2014-01-29Adding a smartmap[i] operator to maps.Pierre-Marie Pédrot
2014-01-28Fixing dependent inversion. Some exceptions were not caught by the tacticPierre-Marie Pédrot
monad.
2014-01-27Abstracting away coercion indexes in Classops.Pierre-Marie Pédrot
2014-01-26Coercions: avoid imperative data structureEnrico Tassi
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-26CoqIDE: command line for extra coqtop "flags"Enrico Tassi
Like the socket for the OCaml debugger
2014-01-26break > 80 cols lineEnrico Tassi
2014-01-26STM: ported to spawnEnrico Tassi
2014-01-26CoqIDE: ported to spawnEnrico Tassi
2014-01-26Spawn: managed processesEnrico Tassi
The Spawn and Spawned modules factor the operation of spawning a process. Both synchronous and asynchronous channels are supported. Both threaded and glib like main loop models are supported. Still, not all combinations are truly tested not equipped with a decent API: only async + glib and sync + thread are, since these are the models we use for coqide<->coqtop and coqtop<->worker respectively.
2014-01-26configure.ml fixed wrt Win32 + byte-only + coqideEnrico Tassi
2014-01-25Adding a test for bug #3023.Pierre-Marie Pédrot
2014-01-25More in CHANGES.Pierre-Marie Pédrot
2014-01-24[Coercion]s use [Sortclass], not [Prop] (in docs)Jason Gross
Reported By: J. Ian Johnson
2014-01-24The configure script now outputs the parameters it was fed with inPierre-Marie Pédrot
config/coq_config.ml
2014-01-20bug correction in proving principles of functionjforest
2014-01-19Using full paths in coqdep -dumpgraph.Pierre-Marie Pédrot
2014-01-19Fixing coqdep graph printing. The transitive reduction algorithm was bugged.Pierre-Marie Pédrot
2014-01-19Adding a default object to generic argument registering mechanism.Pierre-Marie Pédrot
2014-01-19Fixing an interpretation bug with tactics in notations. For some obscurePierre-Marie Pédrot
reason, Ltac interpretation does not allow tactics of the following shape : let x := bla in TacGeneric tac. Hence we force genargs to be tactics and build the resulting hole tactic from scratch.
2014-01-19Fixing checker compilation, which was broken by the following commit:Pierre-Marie Pédrot
05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
2014-01-18Relaxing the sort elimination check to allow for let-bindings in arities.Maxime Dénès
I restored this in the kernel, and added it to the checker. There is one last source of non-uniformity, which is the Sort case in the checker (was not present in the kernel). I don't know what this case covers, so it should be reviewed.
2014-01-18Makefiles use $(foo), not $foo, for variablesJason Gross
Also, we need :=, so that it's evaluated immediately, rather than becoming a self-recursive variable. This fixes the "Undefined variable 'C'" error that make keeps spewing.
2014-01-18Fixup make clean and .merlinPierre Boutillier
2014-01-17Follow-up of bugfix for #3204: local definitions were not handled properly.Pierre-Marie Pédrot
2014-01-17Fixing bug #1758: Print Hint output can be misleading if variable shadows ↵Pierre-Marie Pédrot
hypothesis.
2014-01-17Update .mailmap with recent contributors.Arnaud Spiwack
I should have updated everyone who committed since the migration to git (giving me a canonical email). I've search git shortlog -s to ensure the best I could that there are no duplicate. I discovered that email addresses from the mailmap are uncapitalised whereas the unmodified addresses are not, creating two different authors for no reason. So, I've added some record to normalise the canonical email addresses when needed.
2014-01-16Fixing bugs #1039: Hypotheses don't respect Barendregt conventionPierre-Marie Pédrot
and #3204: Failure of hygiene condition. It was sufficient to tweak a flag in the constr externalization...
2014-01-16Implementing transitive reduction in the dependency graph printingPierre-Marie Pédrot
mechanism of coqdep.
2014-01-15Christmas is over...Maxime Dénès
2014-01-15Test case containing a proof of false due to a DeBruijn off-by-one error in theMaxime Dénès
code checking allowed sorts for elimination.
2014-01-14-schedule-vi-checking generates better scriptEnrico Tassi
2014-01-14STM: fix -async-proofs lazyEnrico Tassi
2014-01-14Removing unused tactics in rewrite.Pierre-Marie Pédrot
2014-01-13Make Require verbosePierre Boutillier
2014-01-13rename Paral-ITP demo fileEnrico Tassi
2014-01-13Paral-ITP demo: better commentsEnrico Tassi
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-13Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Pierre Boutillier
The exact filename has to be written. This is coherent with the RefMan.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:10:48 +0000