diff options
| author | vblot <24938579+vblot@users.noreply.github.com> | 2021-05-28 18:29:37 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-28 18:29:37 +0200 |
| commit | e12110637730d067c216abcc86185b761189b342 (patch) | |
| tree | c9ed415bbdadb2801e4917aae4a803035b13d4e8 /doc | |
| parent | 52980aab9541a12619eb9191a94e9b2ba4684447 (diff) | |
| download | smtcoq-e12110637730d067c216abcc86185b761189b342.tar.gz smtcoq-e12110637730d067c216abcc86185b761189b342.zip | |
getting rid of native-coq (#95)
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sources.md | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/doc/sources.md b/doc/sources.md index 55d2cec..045150d 100644 --- a/doc/sources.md +++ b/doc/sources.md @@ -17,14 +17,6 @@ The rest of the document describes the organization of `src`. SMTCoq sources are contained in this directory. A few Coq files can be found at top-level. -### [configure.sh](../src/configure.sh) - -This script is meant to be run when compiling SMTCoq for the first time. It -should also be run every time the Makefile is modified. It takes as argument an -optional flag `-native` which, when present, will set up the sources to use the -*native Coq* libraries. Otherwise the standard version 8.5 of Coq is used. See -section [versions](#versions). - ### [SMTCoq.v](../src/SMTCoq.v) This is the main SMTCoq entry point, it is meant to be imported by users that @@ -142,30 +134,6 @@ This module contains miscellaneous general lemmas that are used in several places throughout the development of SMTCoq. -### [versions](../src/versions) - -This directory contains everything that is dependent on the version of Coq that -one wants to use. `standard` contains libraries for the standard version of Coq -and `native` contains everything related to native Coq. Note that some -libraries are already present in the default libraries of native Coq, in this -case they have a counterpart in `standard` that replicates the functionality -(without using native integers or native arrays). - -A particular point of interest is the files -[smtcoq_plugin_standard.ml4](../src/versions/standard/smtcoq_plugin_standard.ml4) -and -[smtcoq_plugin_native.ml4](../src/versions/native/smtcoq_plugin_native.ml4). They -provide extension points for Coq by defining new vernacular commands and new -tactics. For instance the tactic `verit` tells Coq to call the OCaml function -`verit.tactic` (which in turns uses the Coq API to manipulate the goals and -call the certified checkers). - -```ocaml -TACTIC EXTEND Tactic_verit -| [ "verit" ] -> [ Verit.tactic () ] -END -``` - ### [spl](../src/spl) |