coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-05-04	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot

2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot

2016-01-20	Update copyright headers.	Maxime Dénès

2016-01-17	Getting rid of the awkward unpack mechanism from Genarg.	Pierre-Marie Pédrot

2015-12-28	Implementing non-focussed generic arguments.	Pierre-Marie Pédrot
	Kind of enhances the situation of bug #4409. Now arguments can be interpreted globally or focussedly in a dynamic fashion because the interpretation function returns a Ftactic.t. The bug is not fixed yet because we should tweak the interpretation of tactic arguments.
2015-12-21	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot

2015-01-12	Update headers.	Maxime Dénès

2014-08-29	Simplification of Genarg unpackers.	Pierre-Marie Pédrot
	Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types.
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2014-01-19	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot

2013-06-30	Using functors to reduce the boilerplate used in registering	ppedrot
	generic argument stuff, including the unsafe Obj.magic-like casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16614 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-22	Now, idtac closures use maps instead of association list.	ppedrot
	The semantics changed slightly so it may break some scripts, though it is very unlikely, as they would have to be quite intricated and poorly written. Indeed, the test-suite passed just fine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16604 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21	Splitted up Genarg in four different levels:	ppedrot
	1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7