diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-25 10:16:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-25 10:16:57 +0200 |
| commit | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (patch) | |
| tree | 705a2b2de824b39d97a28fcea3b8287b53204b54 | |
| parent | 7d2dfd6fabd5d447166b1cb0e3b2993cc8abf4b3 (diff) | |
| parent | 069ab52e2af900d498395ebd1b00b7983152326e (diff) | |
Merge PR #6009: Master+misc typos dead code etc
| -rw-r--r-- | kernel/context.ml | 5 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 5 | ||||
| -rw-r--r-- | vernac/record.ml | 1 |
4 files changed, 7 insertions, 6 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 929324efe..d635c4515 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -379,8 +379,9 @@ struct (** Return the number of {e local declarations} in a given named-context. *) let length = List.length -(** Return a declaration designated by a given de Bruijn index. - @raise Not_found if the designated identifier is not present in the designated named-context. *) let rec lookup id = function +(** Return a declaration designated by a given identifier + @raise Not_found if the designated identifier is not present in the designated named-context. *) + let rec lookup id = function | decl :: _ when Id.equal id (Declaration.get_id decl) -> decl | _ :: sign -> lookup id sign | [] -> raise Not_found diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 63b8cc482..18bb7d2db 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -203,7 +203,7 @@ module PatternMatching (E:StaticEnvironment) = struct let pick l = pick l imatching_error - (** Declares a subsitution, a context substitution and a term substitution. *) + (** Declares a substitution, a context substitution and a term substitution. *) let put subst context terms : unit m = let s = { subst ; context ; terms ; lhs = () } in { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s } diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 2077526db..fdaeded87 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -807,7 +807,8 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - str |> Global.lookup_named |> NamedDecl.set_id str |> print_named_decl + str |> Global.lookup_named |> print_named_decl + with Not_found -> user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -839,7 +840,7 @@ let print_opaque_name qid = let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl + env |> lookup_named id |> print_named_decl let print_about_any ?loc k = match k with diff --git a/vernac/record.ml b/vernac/record.ml index 9a8657c3c..5533fe5b3 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -418,7 +418,6 @@ let declare_structure finite univs id idbuild paramimpls params arity template begin let env = Global.env () in let env' = Environ.push_context ctx env in - (* let env'' = Environ.push_rel_context params env' in *) let evd = Evd.from_env env' in Inductiveops.infer_inductive_subtyping env' evd mie end |