coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-09-06	Fix coq/ltac2#23: Int.compare should not be uniformly 0.	Pierre-Marie Pédrot
	Stupid typo.
2017-09-06	Using higher-order representation for closures.	Pierre-Marie Pédrot

2017-09-06	Parameterizing over parameters in ML functions from Tac2core.	Pierre-Marie Pédrot

2017-09-06	The interp_app function now takes a closure as an argument.	Pierre-Marie Pédrot

2017-09-06	Moving Tac2ffi before Tac2interp.	Pierre-Marie Pédrot

2017-09-06	Introducing abstract data representations.	Pierre-Marie Pédrot

2017-09-06	Code factorization.	Pierre-Marie Pédrot

2017-09-05	Refine does not evar-normalizes the goal preemptively.	Pierre-Marie Pédrot

2017-09-05	Binding the firstorder tactic.	Pierre-Marie Pédrot

2017-09-05	Binding move and intro.	Pierre-Marie Pédrot

2017-09-05	Introducing quotations for move locations.	Pierre-Marie Pédrot

2017-09-05	Binding the inversion family of tactics.	Pierre-Marie Pédrot

2017-09-05	Typeclasses_eauto strategy is now optional.	Pierre-Marie Pédrot

2017-09-05	Quotations for auto-related tactics.	Pierre-Marie Pédrot

2017-09-05	More static invariants for typeclass_eauto.	Pierre-Marie Pédrot

2017-09-05	ML bindings of auto-related tactics.	Pierre-Marie Pédrot

2017-09-04	More notations for primitive tactics.	Pierre-Marie Pédrot

2017-09-04	More precise error messages for scope failure.	Pierre-Marie Pédrot

2017-09-04	Implementing the non-strict mode.	Pierre-Marie Pédrot

2017-09-04	Better backtraces for a few datatypes.	Pierre-Marie Pédrot

2017-09-04	Quick-and-dirty backtrace mechanism for the interpreter.	Pierre-Marie Pédrot

2017-09-04	Closures now wear the constant they originated from.	Pierre-Marie Pédrot

2017-09-04	Fix coq/ltac2#17: Assertion failed. on only shelved goals remaining.	Pierre-Marie Pédrot
	We check that the goal tactic is focussed before calling enter_one.
2017-09-04	Implementing lazy matching over terms.	Pierre-Marie Pédrot

2017-09-04	Proper anomalies for missing registered primitives.	Pierre-Marie Pédrot

2017-09-03	Introducing a macro for constr matching.	Pierre-Marie Pédrot

2017-09-03	Moving generic arguments to Tac2quote.	Pierre-Marie Pédrot

2017-09-03	Uniform handling of locations in the various AST.	Pierre-Marie Pédrot

2017-09-03	Allowing ML objects to return mere tactic expressions.	Pierre-Marie Pédrot

2017-09-03	Allowing complex types in ML objects.	Pierre-Marie Pédrot

2017-09-03	Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in anomalies.	Pierre-Marie Pédrot

2017-09-02	Fix coq/ltac2#12: Error should name which match cases are unhandled.	Pierre-Marie Pédrot

2017-09-02	Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.	Pierre-Marie Pédrot
	Instead of setting globally the option, we add a hook to set it in the init object of the plugin.
2017-09-01	Ensuring the Ltac definitions have lowercase names.	Pierre-Marie Pédrot

2017-08-31	Properly handling internal errors from Coq.	Pierre-Marie Pédrot

2017-08-31	Expand the primitive functions on terms.	Pierre-Marie Pédrot

2017-08-31	Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across ↵	Pierre-Marie Pédrot
	`Require`.
2017-08-31	Fix coq/ltac2#3: Constructor expects n arguments should name which ↵	Pierre-Marie Pédrot
	constructor it is.
2017-08-30	Binding reduction functions acting on terms.	Pierre-Marie Pédrot

2017-08-29	Fix printing of Ltac2 in quotations.	Pierre-Marie Pédrot

2017-08-29	Fixing printing of tactic expressions.	Pierre-Marie Pédrot

2017-08-29	Centralizing tag declarations.	Pierre-Marie Pédrot

2017-08-29	Rolling our own generic arguments.	Pierre-Marie Pédrot

2017-08-29	Rolling our own dynamic types for Ltac2.	Pierre-Marie Pédrot
	This prevents careless confusions with generic arguments from Coq.
2017-08-29	Pass Ltac2 variables in a dedicated environment for generic arguments.	Pierre-Marie Pédrot
	This is a way to hack around the fact that various interpretation functions rely wrongly on the values of the environment to do nasty tricks. Typically, the interpretation of terms is broken, as it will fail when there is a bound variable with the same name as a hypothesis, instead of producing the hypothesis itself.
2017-08-29	Removing dead code for handling of array litterals.	Pierre-Marie Pédrot

2017-08-29	Factorizing code for declaration of primitive tactics.	Pierre-Marie Pédrot

2017-08-29	Implementing Ltac2 antiquotations in constr syntax.	Pierre-Marie Pédrot

2017-08-29	Binding an unsafe substitution function.	Pierre-Marie Pédrot

2017-08-29	Binding primitives to generate fresh variables.	Pierre-Marie Pédrot