diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 38 | ||||
| -rw-r--r-- | stm/stm.mli | 8 |
2 files changed, 21 insertions, 25 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index fc539b5208..e32b6c9f1c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1837,22 +1837,18 @@ end = struct (* {{{ *) let o = match c.Declarations.const_body with | Declarations.OpaqueDef o -> o | _ -> assert false in - let uc = - Option.get - (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in + (* No need to delay the computation, the future has been forced by + the call to [check_task_aux] above. *) + let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in + let uc = Univ.hcons_universe_context_set uc in (* We only manipulate monomorphic terms here. *) let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in - let pr = - Future.from_val (map (Option.get (Global.body_of_constant_body c))) in - let uc = - Future.chain uc Univ.hcons_universe_context_set in - let pr = Future.chain pr discharge in - let pr = Future.chain pr Constr.hcons in - Future.sink pr; - let extra = Future.join uc in - u.(bucket) <- uc; - p.(bucket) <- pr; - u, Univ.ContextSet.union cst extra, false + let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in + let pr = discharge pr in + let pr = Constr.hcons pr in + u.(bucket) <- Some uc; + p.(bucket) <- Some pr; + u, Univ.ContextSet.union cst uc, false let check_task name l i = match check_task_aux "" name l i with @@ -2661,16 +2657,16 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initalization routine *) +(* Main initialization routine *) type stm_init_options = { (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should dissappear at some + specified [doc_type]. This distinction should disappear at some some point. *) doc_type : stm_doc_type; (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -2702,8 +2698,8 @@ let dirpath_of_file f = Loadpath.logical lp with Not_found -> Libnames.default_root_prefix in - let file = Filename.chop_extension (Filename.basename f) in - let id = Id.of_string file in + let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in + let id = Id.of_string f in let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir @@ -2728,7 +2724,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Mltop.add_coq_path iload_path; + List.iter Loadpath.add_coq_path iload_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; @@ -3117,7 +3113,7 @@ let ind_len_loc_of_id sid = let compute_indentation ?loc sid = Option.cata (fun loc -> let open Loc in - (* The effective lenght is the lenght on the last line *) + (* The effective length is the length on the last line *) let len = loc.ep - loc.bp in let prev_indent = match ind_len_loc_of_id sid with | None -> 0 diff --git a/stm/stm.mli b/stm/stm.mli index a0bbe05b3a..5e1e9bf5ad 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -50,7 +50,7 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initalization options: +(** Coq initialization options: - [doc_type]: Type of document being created. @@ -63,13 +63,13 @@ type stm_doc_type = *) type stm_init_options = { (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should dissappear at some + specified [doc_type]. This distinction should disappear at some some point. *) doc_type : stm_doc_type; (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -86,7 +86,7 @@ type stm_init_options = { (** The type of a STM document *) type doc -(** [init_core] performs some low-level initalization; should go away +(** [init_core] performs some low-level initialization; should go away in future releases. *) val init_core : unit -> unit |