aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-08 18:14:53 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-08 18:14:53 +0200
commit9fe0471ef0127e9301d0450aacaeb1690abb82ad (patch)
tree6a244976f5caef6a2b88c84053fce87f94c78f96 /plugins/firstorder
parenta6de02fcfde76f49b10d8481a2423692fa105756 (diff)
parent8d3f0b614d7b2fb30f6e87b48a4fc5c0d286e49c (diff)
Change the toplevel representation of Ltac values to an untyped one.
This brings the evaluation model of Ltac closer to those of usual languages, and further allows the integration of static typing in the long run. More precisely, toplevel constructed values such as lists and the like do not carry anymore the type of the underlying data they contain. This is mostly an API change, as it did not break any contrib outside of mathcomp.
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 587d10d1c..b04c4a50c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -122,6 +122,7 @@ let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma
let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
ARGUMENT EXTEND firstorder_using
+ TYPED AS reference_list
PRINTED BY pr_firstorder_using_typed
RAW_TYPED AS reference_list
RAW_PRINTED BY pr_firstorder_using_raw