diff options
| -rw-r--r-- | engine/evd.ml | 33 | ||||
| -rw-r--r-- | engine/evd.mli | 1 | ||||
| -rw-r--r-- | proofs/clenv.ml | 38 |
3 files changed, 38 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 diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 16146f4846..0697c94d74 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -432,6 +432,44 @@ let check_bindings bl = str " occurs more than once in binding list.") | [] -> () +let explain_no_such_bound_variable evd id = + let fold l (n, clb) = + let na = match clb with + | Cltyp (na, _) -> na + | Clval (na, _, _) -> na + in + if na != Anonymous then out_name na :: l else l + in + let mvl = List.fold_left fold [] (Evd.meta_list evd) 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 fold (l1, l2 as l) (n, clb) = + let (na',def) = match clb with + | Cltyp (na, _) -> (na, false) + | Clval (na, _, _) -> (na, true) + in + if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) + else l + in + let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) 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 meta_of_binder clause loc mvs = function | NamedHyp s -> meta_with_name clause.evd s | AnonHyp n -> |