diff options
| author | herbelin | 2000-01-26 15:01:55 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-26 15:01:55 +0000 |
| commit | daf4ef5bb4138eb2ab9b7bf39d1c6a08984b8c01 (patch) | |
| tree | 08b8482a9e974697f961993d039e7274ea1e1d99 /parsing | |
| parent | 40183da6b54d8deef242bac074079617d4a657c2 (diff) | |
Abstraction de l'implémentation des signatures de Sign en vue intégration du let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pretty.ml | 3 | ||||
| -rw-r--r-- | parsing/printer.ml | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 2fc7063373..86f5981feb 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -95,7 +95,8 @@ let print_env pk = prec (gLOB nil_sign) let assumptions_for_print lna = - ENVIRON(([],[]),List.map (fun na -> (na,())) lna) + List.fold_right (fun na env -> add_rel (na,()) env) lna + (ENVIRON(nil_sign,nil_dbsign)) let print_constructors_with_sep pk fsep mip = let pterm,pterminenv = diff --git a/parsing/printer.ml b/parsing/printer.ml index c93fdbb480..3083154e60 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -176,7 +176,7 @@ let pr_env k env = [< sign_env; db_env >] let pr_ne_env header k = function - | ENVIRON (([],[]),[]) -> [< >] + | ENVIRON (sign,_) as env when isnull_sign sign & isnull_rel_env env -> [< >] | env -> let penv = pr_env k env in [< header; penv >] let pr_env_limit n env = |