| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-04 | follows G. Gilbert's suggestion to have polymorphism following a flag | Yves Bertot | |
| 2018-05-04 | A modified version that includes code proposed by G. Gilbert | Yves Bertot | |
| 2018-05-04 | This revision contains a simple Check command. | Yves Bertot | |
| 2018-05-03 | little cleanup on the defining command, and question in comments | Yves Bertot | |
| 2018-05-03 | Merge PR #7134: When an error comes from loading the prelude, tell it ↵ | Emilio Jesus Gallego Arias | |
| happened at initialization time | |||
| 2018-05-03 | This version contains a simple command that defines a new constant | Yves Bertot | |
| 2018-05-03 | Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_subst | Pierre-Marie Pédrot | |
| 2018-05-03 | Fix #7415. Printing Width was not applied to error messages. | Pierre Courtieu | |
| 2018-05-03 | Add .byte targets for every bestocaml target | Gaëtan Gilbert | |
| This makes it easier to compile our executables for debug purposes. | |||
| 2018-05-03 | Merge PR #7304: Make `intro`/`intros` progress on existential variables. | Pierre-Marie Pédrot | |
| 2018-05-03 | Fixes issue #7083 / Windows build: Unify build logging to console (for ↵ | Michael Soegtrop | |
| appveyor) and files | |||
| 2018-05-03 | Fixes issue #7081 / Windows build: strip in lablgtk build can fail randomly | Michael Soegtrop | |
| 2018-05-03 | Merge PR #7400: ci-vst.sh: use -o progs | Emilio Jesus Gallego Arias | |
| 2018-05-03 | Merge PR #7402: [ci]: add pidetop (fix #7336) | Emilio Jesus Gallego Arias | |
| 2018-05-02 | Making explicit that errors happen in one of five executation phases. | Hugo Herbelin | |
| The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase. | |||
| 2018-05-02 | Reporting when an error occurs at initialization time. | Hugo Herbelin | |
| Done by simplifying the three "try" liable to be caught at initialization time into one and by ensuring that the remaining one reports about being in initialization phase. | |||
| 2018-05-02 | Make "intro"/"intros" progress on existential variables. | Hugo Herbelin | |
| 2018-05-02 | [ci]: add pidetop (fix #7336) | Enrico Tassi | |
| 2018-05-02 | Fix #7214: install knows which ml files do not get compiled to cmx. | Gaëtan Gilbert | |
| 2018-05-02 | Remove unused Deque files | Gaëtan Gilbert | |
| 2018-05-02 | Merge PR #7339: [api] Move bullets and goals selectors to `proofs/` | Théo Zimmermann | |
| 2018-05-02 | Merge PR #7403: Makefile doc owners | Théo Zimmermann | |
| 2018-05-02 | first examples of commands taking arguments | Yves Bertot | |
| 2018-05-02 | Fix Makefile.ci pattern in CODEOWNERS | Maxime Dénès | |
| 2018-05-02 | Make doc owners also own Makefile.doc | Maxime Dénès | |
| 2018-05-02 | Merge PR #7394: [ci] [travis] Install num by default in all switches. | Gaëtan Gilbert | |
| 2018-05-02 | Merge PR #7370: Fix PHONY typo in coq_makefile | Enrico Tassi | |
| 2018-05-01 | add usage explanations | Yves Bertot | |
| 2018-05-01 | Merge PR #7305: [toplevel] improve indentation | Emilio Jesus Gallego Arias | |
| 2018-05-01 | add a simple explanation in the README file | Yves Bertot | |
| 2018-05-01 | a first project on how to organize files and define a simple query | Yves Bertot | |
| 2018-05-01 | Automatically run alienclean before compiling. | Gaëtan Gilbert | |
| This removes the "leftover files without known source" error in favor of automatic handling. | |||
| 2018-05-01 | Actually take advantage of the normalization status of kernel closures. | Pierre-Marie Pédrot | |
| We know that when a fterm is marked as Whnf or Norm, the only thing that can happen in the reduction machine is administrative reduction pushing the destructured term on the stack. Thus there is no need to perform any actual performative reduction. Furthermore, every head subterm of those terms are recursively Whnf or Norm, which implies that no update mark is pushed on the stack during the destructuration. So there is no need to unzip the stack to unset FLOCKED nodes as well. | |||
| 2018-05-01 | ci-vst.sh: use -o progs | Gaëtan Gilbert | |
| This is closer to what we mean than reproducing the default target without progs. | |||
| 2018-05-01 | Merge PR #7397: [ci] Fix #7396: VST is broken | Gaëtan Gilbert | |
| 2018-05-01 | [ci] Fix #7396: VST is broken | Emilio Jesus Gallego Arias | |
| This is due to our CI script relying on their makefile internals, unfortunately we still have to do this to avoid timeouts. | |||
| 2018-05-01 | [api] Move bullets and goals selectors to `proofs/` | Emilio Jesus Gallego Arias | |
| `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select` | |||
| 2018-04-30 | [ci] [travis] Install num by default in all switches. | Emilio Jesus Gallego Arias | |
| This makes sense and simplifies the script a bit. In preparation for a more uniform, Docker-based base image. | |||
| 2018-04-30 | Merge PR #7379: [doc] Update Sphinx build instructions for Debian derivatives. | Théo Zimmermann | |
| 2018-04-30 | Merge PR #6935: Separate universe minimization and evar normalization functions | Pierre-Marie Pédrot | |
| 2018-04-30 | Adapt the VM GC hook to handle the no-naked-pointers option flag. | Pierre-Marie Pédrot | |
| The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers to C-allocated strings standing for VM bytecode. If the the no-naked-pointers option is set, we perform the check that a stack value lives on the OCaml heap ourselves. | |||
| 2018-04-30 | Make the VM accumulator look like an OCaml block. | Pierre-Marie Pédrot | |
| We allocate an additional header so that the accumulator is not a naked pointer. Indeed, it is contained in accumulator blocks which are scanned by the GC as their tags is 0. | |||
| 2018-04-30 | Wrap VM bytecode used on the OCaml side in an OCaml block. | Pierre-Marie Pédrot | |
| This prevents the existence of a few naked pointers to C heap from the OCaml heap. VM bytecode is represented as any block of size at least 1 whose first field points to a C-allocated string. This representation is compatible with the Coq VM representation of (potentially recursive) closures, which are already specifically tailored in the OCaml GC to be able to contain out-of-heap data. | |||
| 2018-04-30 | Merge PR #6944: Strict focusing using Default Goal Selector. | Pierre-Marie Pédrot | |
| 2018-04-30 | Merge PR #7355: [owners] Makefile.ci belongs to the CI category. | Maxime Dénès | |
| 2018-04-30 | Merge PR #6958: [lib] Move global options to their proper place. | Maxime Dénès | |
| 2018-04-30 | [doc] Update Sphinx build instructions for Debian derivatives. | Emilio Jesus Gallego Arias | |
| We update the instructions a bit providing the name of the Debian packages, we also mention Nix and add to .gitignore a Sphinx-autogenerated file. | |||
| 2018-04-30 | Merge PR #7381: [gitlab] Update base image to Ubuntu bionic + some improvements. | Gaëtan Gilbert | |
| 2018-04-29 | Strict focusing using Default Goal Selector. | Gaëtan Gilbert | |
| We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689. | |||
| 2018-04-29 | tclSELECT: SelectAll never happens | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |