From 940b2f972c4b3f42850e36c721564b127d30e496 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 6 Mar 2018 13:41:37 +0100
Subject: An experimental 'Show Extraction' command (grant feature wish #4129)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

 Attempt to extract the current ongoing proof (request by
 Clément Pit-Claudel on coqdev, and also #4129).
 Evars are handled as axioms.
---
 plugins/extraction/table.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction/table.ml')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 5903733a6..730e7b395 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -36,14 +36,13 @@ module Refset' = Refset_env
 let occur_kn_in_ref kn = function
   | IndRef (kn',_)
   | ConstructRef ((kn',_),_) -> MutInd.equal kn kn'
-  | ConstRef _ -> false
-  | VarRef _ -> assert false
+  | ConstRef _ | VarRef _ -> false
 
 let repr_of_r = function
   | ConstRef kn -> Constant.repr3 kn
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
-  | VarRef _ -> assert false
+  | VarRef v -> KerName.repr (Lib.make_kn v)
 
 let modpath_of_r r =
   let mp,_,_ = repr_of_r r in mp
@@ -277,7 +276,7 @@ let safe_basename_of_global r =
     | ConstructRef ((kn,i),j) ->
       (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
        with Not_found -> last_chance r)
-    | VarRef _ -> assert false
+    | VarRef v -> v
 
 let string_of_global r =
  try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r)
-- 
cgit v1.2.3