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

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

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