diff options
| author | herbelin | 2011-10-10 22:00:04 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-10 22:00:04 +0000 |
| commit | d74f1da437c214cc0c960e87e8bbf04dd214128e (patch) | |
| tree | 017dc70a7db4dc08a1f414aeacec631a47bc91ad /pretyping/evd.ml | |
| parent | 32bcb10ce3470377314b964223ce9aed1ab33c72 (diff) | |
Passed conv_algo to evar_define and move call to solve_refl to
evar_define so that it can recursively deal with evar/evar problems.
Also, check_evar_instance now called after each instantiation.
Also did a bit of file reformatting.
The commit apparently induces a loss of some 0,4% on the compilation
of the standard library. Maybe, introducing a heuristic to decide when
to call check_evar_instance (which I guess is responsible for the
overhead) might be a good thing to look at?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 817ee97035..ac604466d3 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -825,9 +825,9 @@ let pr_evar_map_t depth sigma = in evs ++ svs ++ cs let print_env_short env = - let pr_body = function None -> mt () | Some b -> str " := " ++ print_constr b in - let pr_named_decl (n, b, _) = pr_id n ++ pr_body b in - let pr_rel_decl (n, b, _) = pr_name n ++ pr_body b in + let pr_body n = function None -> pr_name n | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in + let pr_named_decl (n, b, _) = pr_body (Name n) b in + let pr_rel_decl (n, b, _) = pr_body n b in let nc = List.rev (named_context env) in let rc = List.rev (rel_context env) in str "[" ++ prlist_with_sep pr_spc pr_named_decl nc ++ str "]" ++ spc () ++ |