diff options
| -rw-r--r-- | .github/CODEOWNERS | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 2 | ||||
| -rw-r--r-- | doc/changelog/05-tactic-language/10002-ltac2.rst | 9 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 46 |
4 files changed, 39 insertions, 20 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 06a733be45..2a325f2d71 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -173,6 +173,8 @@ azure-pipelines.yml @coq/ci-maintainers /plugins/rtauto/ @PierreCorbineau # Secondary maintainer @herbelin +/user-contrib/Ltac2 @ppedrot + ########## Pretyper ########## /pretyping/ @mattam82 diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 95fceb773a..fa39b41565 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,7 +215,7 @@ ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=dev}" +: "${simple_io_CI_REF:=master}" : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" diff --git a/doc/changelog/05-tactic-language/10002-ltac2.rst b/doc/changelog/05-tactic-language/10002-ltac2.rst new file mode 100644 index 0000000000..6d62f11eff --- /dev/null +++ b/doc/changelog/05-tactic-language/10002-ltac2.rst @@ -0,0 +1,9 @@ +- Ltac2, a new version of the tactic language Ltac, that doesn't + preserve backward compatibility, has been integrated in the main Coq + distribution. It is still experimental, but we already recommend + users of advanced Ltac to start using it and report bugs or request + enhancements. See its documentation in the :ref:`dedicated chapter + <ltac2>` (`#10002 <https://github.com/coq/coq/pull/10002>`_, plugin + authored by Pierre-Marie Pédrot, with contributions by various + users, integration by Maxime Dénès, help on integrating / improving + the documentation by Théo Zimmermann and Jim Fehrle). diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 759cbe22ee..824400b4e3 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -231,7 +231,7 @@ let check_engagement env expected_impredicative_set = type side_effect = { from_env : Declarations.structure_body CEphemeron.key; seff_constant : Constant.t; - seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body; + seff_body : Constr.t Declarations.constant_body; seff_role : Entries.side_effect_role; } @@ -299,11 +299,6 @@ let concat_private = SideEffects.concat let universes_of_private eff = let fold acc eff = - let acc = match eff.seff_body.const_body with - | Def _ -> acc - | OpaqueDef (_, ctx) -> ctx :: acc - | Primitive _ | Undef _ -> assert false - in match eff.seff_body.const_universes with | Monomorphic ctx -> ctx :: acc | Polymorphic _ -> acc @@ -601,7 +596,7 @@ let inline_side_effects env body side_eff = let fold (subst, var, ctx, args) (c, cb) = let (b, opaque) = match cb.const_body with | Def b -> (Mod_subst.force_constr b, false) - | OpaqueDef (b, _) -> (b, true) + | OpaqueDef b -> (b, true) | _ -> assert false in match cb.const_universes with @@ -689,13 +684,13 @@ let constant_entry_of_side_effect eff = | Polymorphic auctx -> Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in - let pt = + let p = match cb.const_body with - | OpaqueDef (b, c) -> b, c - | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty + | OpaqueDef b -> b + | Def b -> Mod_subst.force_constr b | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, ()); + const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; @@ -721,11 +716,6 @@ let export_side_effects mb env (b_ctx, eff) = match cb.const_universes with | Polymorphic _ -> env | Monomorphic ctx -> - let ctx = match eff.seff_body.const_body with - | Def _ -> ctx - | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx - | Undef _ | Primitive _ -> assert false - in Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = @@ -737,7 +727,12 @@ let export_side_effects mb env (b_ctx, eff) = let kn = eff.seff_constant in let ce = constant_entry_of_side_effect eff in let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in - let cb = map_constant Future.force cb in + let map cu = + let (c, u) = Future.force cu in + let () = assert (Univ.ContextSet.is_empty u) in + c + in + let cb = map_constant map cb in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) in @@ -755,7 +750,7 @@ let n_univs cb = match cb.const_universes with let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val p)) cb) in + let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in let bodies = List.map map exported in let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in @@ -794,7 +789,20 @@ let add_constant ?role ~in_section l decl senv = let eff = match role with | None -> empty_private_constants | Some role -> - let cb = map_constant Future.force cb in + let body, univs = match cb.const_body with + | (Primitive _ | Undef _) -> assert false + | Def c -> (Def c, cb.const_universes) + | OpaqueDef o -> + let (b, ctx) = Future.force o in + match cb.const_universes with + | Monomorphic ctx' -> + OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') + | Polymorphic auctx -> + (* Upper layers enforce that there are no internal constraints *) + let () = assert (Univ.ContextSet.is_empty ctx) in + OpaqueDef b, Polymorphic auctx + in + let cb = { cb with const_body = body; const_universes = univs } in let from_env = CEphemeron.create senv.revstruct in let eff = { from_env = from_env; |