diff options
| author | mdenes | 2013-01-22 17:37:00 +0000 |
|---|---|---|
| committer | mdenes | 2013-01-22 17:37:00 +0000 |
| commit | 6b908b5185a55a27a82c2b0fce4713812adde156 (patch) | |
| tree | c2857724d8b22ae3d7a91b3a683a57206caf9b54 /printing | |
| parent | 62ce65dadb0afb8815b26069246832662846c7ec (diff) | |
New implementation of the conversion test, using normalization by evaluation to
native OCaml code.
Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e7f4a0b245..9f6715a7d9 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -258,7 +258,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,k,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c, (CastConv t|CastVM t)) -> c, t + | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t | _ -> c, CHole (Loc.ghost, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) @@ -540,6 +540,7 @@ let pr pr sep inherited a = match b with | CastConv b -> str ":" ++ pr mt (-lcast,E) b | CastVM b -> str "<:" ++ pr mt (-lcast,E) b + | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b | CastCoerce -> str ":>"), lcast | CNotation (_,"( _ )",([t],[],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom @@ -637,6 +638,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function | Red true -> error "Shouldn't be accessible from user." | ExtraRedExpr s -> str s | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o + | CbvNative o -> str "native_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> |