From cf04daec997ae431b14dd3a3bbf0db22013b3c71 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 29 Jul 2014 14:07:42 +0200
Subject: Untyped terms in tactic: function [type_term c] to give a typed
 version of [c].

---
 parsing/g_ltac.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 8b1a1979fb..4be4aa4ae7 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -138,7 +138,8 @@ GEXTEND Gram
   ;
   may_eval_arg:
     [ [ c = constr_eval -> ConstrMayEval c
-      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ]
+      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l
+      | IDENT "type_term"; c=Constr.constr -> TacPretype c ] ]
   ;
   fresh_id:
     [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ]
-- 
cgit v1.2.3