From ae455fa3aa29c872c9c5b2736fff861afebcd051 Mon Sep 17 00:00:00 2001 From: ckeller Date: Fri, 15 Mar 2019 11:23:55 +0100 Subject: V8.9 (#43) * New syntax for implicit arguments * Towards 8.9: problems with Micromega plugin * Move to _CoqProject * Back to name Makefile * Switch to Makefile.local instead of -extra * The compilation issue is a Coq bug * Ok with 8.9 * INSTALL with 8.9 * Everything ok with 8.9 --- src/versions/native/structures.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/versions/native/structures.ml') diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index e11697e..ee4bf96 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -139,10 +139,10 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r = (* Micromega *) -module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega module Micromega_plugin_Micromega = Micromega module Micromega_plugin_Mutils = Mutils +module Micromega_plugin_Certificate = Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega let micromega_coq_proofTerm = Coq_micromega.M.coq_proofTerm -- cgit