diff options
| author | Pierre-Marie Pédrot | 2015-09-27 16:39:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-27 16:47:46 +0200 |
| commit | a3d7630d74b720b771e880dcf0fcad05de553a6e (patch) | |
| tree | 9570c13571d7ab136a0b41b9223d246344d6fa7c /engine | |
| parent | 9cadb903b7c3a3be8014152b293cd5ade3a7c8b7 (diff) | |
Removing meta_with_name from Evd.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 33 | ||||
| -rw-r--r-- | engine/evd.mli | 1 |
2 files changed, 0 insertions, 34 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 9c53006c13..12a04fcc22 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1451,39 +1451,6 @@ let meta_reassign mv (v, pb) evd = let meta_name evd mv = try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous -let explain_no_such_bound_variable evd id = - let mvl = - List.rev (Metamap.fold (fun n clb l -> - let na = fst (clb_name clb) in - if na != Anonymous then out_name na :: l else l) - evd.metas []) in - errorlabstrm "Evd.meta_with_name" - (str"No such bound variable " ++ pr_id id ++ - (if mvl == [] then str " (no bound variables at all in the expression)." - else - (str" (possible name" ++ - str (if List.length mvl == 1 then " is: " else "s are: ") ++ - pr_enum pr_id mvl ++ str")."))) - -let meta_with_name evd id = - let na = Name id in - let (mvl,mvnodef) = - Metamap.fold - (fun n clb (l1,l2 as l) -> - let (na',def) = clb_name clb in - if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) - else l) - evd.metas ([],[]) in - match mvnodef, mvl with - | _,[] -> - explain_no_such_bound_variable evd id - | ([n],_|_,[n]) -> - n - | _ -> - errorlabstrm "Evd.meta_with_name" - (str "Binder name \"" ++ pr_id id ++ - strbrk "\" occurs more than once in clause.") - let clear_metas evd = {evd with metas = Metamap.empty} let meta_merge evd1 evd2 = diff --git a/engine/evd.mli b/engine/evd.mli index cfe4adc09d..bc81bd8189 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -440,7 +440,6 @@ val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_ val meta_type : evar_map -> metavariable -> types val meta_ftype : evar_map -> metavariable -> types freelisted val meta_name : evar_map -> metavariable -> Name.t -val meta_with_name : evar_map -> Id.t -> metavariable val meta_declare : metavariable -> types -> ?name:Name.t -> evar_map -> evar_map val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map |