projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
migrate HaskStrong away from using LeveledHaskType
[coq-hetmet.git]
/
src
/
ExtractionMain.v
diff --git
a/src/ExtractionMain.v
b/src/ExtractionMain.v
index
77326e0
..
4da66c7
100644
(file)
--- a/
src/ExtractionMain.v
+++ b/
src/ExtractionMain.v
@@
-132,7
+132,7
@@
Section core2proof.
OK (eol+++eol+++eol+++
"\begin{preview}"+++eol+++
"$\displaystyle "+++
OK (eol+++eol+++eol+++
"\begin{preview}"+++eol+++
"$\displaystyle "+++
- toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
+ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
" $"+++eol+++
"\end{preview}"+++eol+++eol+++eol)
)))))))).
" $"+++eol+++
"\end{preview}"+++eol+++eol+++eol)
)))))))).
@@
-432,9
+432,9
@@
Section core2proof.
(addErrorMessage ("HaskStrong...")
(let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
(addErrorMessage ("HaskStrong...")
(let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
- hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
+ hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
in (* insert HaskProof-to-HaskProof manipulations here *)
in (* insert HaskProof-to-HaskProof manipulations here *)
- OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ@@nil) _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' =>
(snd e') >>= fun e'' =>
strongExprToWeakExpr hetmet_brak' hetmet_esc'
>>= fun e' =>
(snd e') >>= fun e'' =>
strongExprToWeakExpr hetmet_brak' hetmet_esc'